람다 미적분 : 대입 피하기 대체의 재귀 정의

Question

형식이 지정되지 않은 람다 미적분의 구현을 프로그래밍하는 데 2 ​​주를 보냈습니다.

위키 피 디아에서 제공 한 대체 정의에 잘 맞는 대체를 피하기위한 재귀 적 정의 (즉, 알파 변환 형태로 대체를 사용합니다)를 공식화했을 수도 있습니다. 나는 그것이 매우 명확하고 단순하게 찾을 수 있기 때문에

이 맞다면 누군가가 나를 위해 그것의 정확성을 확인하고 수 있다면 정말 감사하겠습니다,이 정의는 거의 사용되지 않는 이유를 설명.

위키 백과의 정의 :

x[x := N] ≡ N 
y[x := N] ≡ y, if x ≠ y 
(M1 M2)[x := N] ≡ (M1[x := N]) (M2[x := N]) 
(λx.M)[x := N] ≡ λx.M 
(λy.M)[x := N] ≡ λy.(M[x := N]), if x ≠ y, provided y ∉ FV(N) 

내 추가 정의는 캡처 회피을 적용합니다 :

y' ∉ (FV(N) ∪ FV(M)) 
M' ≡ M[y:=y'] 

Answer 1

규칙이 올바른지

(λy.M)[x := N] ≡ λy'.(M'[x := N]), if x ≠ y and y ∈ FV(N) 

.

무료 변수를 추적해야하기 때문에 자주 사용하지 않습니다. 이 구현에서는 이름이 중요하지 않다는 점에서 의미가 반 직관적입니다. 이름이 중심적인 역할을합니다.

아직 조작 상 의미가 표시되지 않았습니다. 이렇게하면 x이 N에 캡처 된 경우 앱 규칙에 (λx.M) N과 같은 앱 규칙이 필요하다는 것을 알 수 있습니다. 그렇다면 알파 이름 바꾸기가 트리거되어야합니다. 여기

문제는 중요한 하나 개의 표현에 너무 많은 (무한) 표현이 존재한다. 이 문제를 해결하는 전형적인 방법 중 하나는 드 브루 지인 지수 (Bruijin index)를 사용하는 것입니다.

https://en.wikipedia.org/wiki/De_Bruijn_index

https://www.chargueraud.org/research/2009/ln/main.pdf

주요 아이디어

는 동일합니다 : 둘 다 바운드 표현의 몫을 하나 개의 표현이 정확히 하나의 표준 양식을 가지도록.