EP
я наверное не правильно изначально задал вопрос, надо было "Как доказать, что какой либо ЯП (Scala) удовлетворяет требованиям α-эквивалентности двух лямбда терм"
Size: a a a
2020 August 11
EB
ну может щас Олег ворвется с напалмом и на своей типовой магии нас всех уничтожит
EP
было бы здорово)
EB
я наверное не правильно изначально задал вопрос, надо было "Как доказать, что какой либо ЯП (Scala) удовлетворяет требованиям α-эквивалентности двух лямбда терм"
у тебя формулировка странная, стравниваешь термы, а пишешь яп должен удовлетворять
EP
ну а как ещё, функциональные литералы в Scala разве не лямбда термы?
E
ну а как ещё, функциональные литералы в Scala разве не лямбда термы?
{
(x: T) => x; x;x;} это разве является лямбда термом?P
Так а что же всё-таки сделать нужно?
P
Или это чисто теоретический интерес?
GP
я хочу сказать что
((x: T) => x) == ((y: T) => y))это эквивалентные лямбда термы в контексте α-эквивалентности
можно по типу эквивалентность доказать
EP
Python
Или это чисто теоретический интерес?
Теоретический
GP
я не уверен, что это то, что тебе надо (плаваю в теории)
GP
а что будет альфа экивалентность для типизированного лямбда выражения? совпадение по типу и по форме?
GP
или просто по типу? (как интересно вообще форма тут будет влиять?)
GP
т.е. наверное просто по типу?
TI
а что будет альфа экивалентность для типизированного лямбда выражения? совпадение по типу и по форме?
Равенство с точностью до замены имени формальной переменной
GP
Равенство с точностью до замены имени формальной переменной
см ниже плз)
TI
Без редукций если я правильно понял
TI
Равенство типов по идее должно доказывать в таком случае
GP
вот мне тоже так показалось