Исчисление лямбда (λa.b) ((λx.xx) (λx.xx))

Question

Im ищет пример слабо нормирующего лямбда-члена. я прав, говоря, что следующее:

(λa.b)((λx.xx)(λx.xx)) 

Сокращает до:

b 

или:

оленья кожа прекращается (если вы пытаетесь уменьшить (λx.xx)(λx.xx))

Я не был уверен, если первое сокращение правильное, так что просто нужно уточнить, спасибо. спасибо.

Answer 1

Если вы оцениваете правильный термин сначала и постоянно, то он никогда не достигнет нормальной формы, поэтому он не является нормализованным. Если вы сначала оцениваете левый член, он немедленно достигнет нормальной формы, поэтому он нормализуется и демонстрирует, что этот термин слабо нормализуется. Это также пример не слияния нетипизированного лямбда-исчисления.

Обратите внимание, что вы, скорее всего, захотите поговорить о том, как система перезаписи нормализуется, чем определенный термин. Таким образом, этот термин является контрпримером сильного нормировочного свойства нетипизированного лямбда-исчисления, но не дает положительного доказательства того, что ULC слабо нормализуется (а это не так).