Feb. 27th, 2016

66george: (киса)
Итого, у меня есть система редукций для лямбда-исчисления, которая мне кажется идеальной. В ней примерно 20 редукций, потому что подстановка выполняется "маленькими шагами" и переименование переменных (там, где нужно их переименовывать) тоже делается в явном виде, это ещё несколько редукций. И теперь я хочу всякие свойства доказать на Агде. Допустим, локальная конфлюэнтность - это примерно 20х20/2=200 случаев, если я правильно считаю. Почти все случаи простые, надо механически выписать проверку. Вроде бы, у кого-то есть программа, чтобы локальную конфлюэнтность проверять автоматически. Или самому написать такую программу и проверить Агдой, что она правильно работает? Или уж сразу написать свой пруфчекер? Или плюнуть и идти страной руководить?

Боюсь объёма предстоящей писанины.

Profile

66george: (Default)
66george

August 2016

S M T W T F S
 1 23456
7 891011 12 13
1415161718 19 20
21 222324252627
28 293031   

Page Summary

Style Credit

Expand Cut Tags

No cut tags
Page generated Jul. 28th, 2017 06:52 am
Powered by Dreamwidth Studios