?

Log in

No account? Create an account
kouzdra [entries|archive|friends|userinfo]
kouzdra

[ website | www.kouzdra.org ]
[ userinfo | livejournal userinfo ]
[ archive | journal archive ]

Примерчик про ATS [Apr. 10th, 2016|12:28 pm]
kouzdra
[Tags|, ]

Известная задачка МакКарти про f91:
fun f91 {i:int} .<max(101-i,0)>. (x: int i)
  : [j:int | (i < 101 && j==91) || (i >= 101 && j==i-10)] int (j) =
  if x >= 101 then x-10 else f91 (f91 (x+11))
// end of [f91]
Приведенный код содержит как раз формальное доказательство завершаемости этой функции - прописан инвариант (max(101-i,0)), который проверямое уменьшается при каждом рекурсивном вызове (max нужна чтобы сделать инвариант натуральным - для целочисленного понятно, что завершаемость не гарантировать - он может выходить в минус сколько угодно).

Это я к этому вопросу - там на сам деле кажется все проще сделано - хватает линейных типов, но как видно с примерчика - возможны и более сложные семантики - причем данный пример тоже из "довольно простых". На полную мощность артиллерия тут близко не используется
LinkReply