Y combinator 어떻게 맞혀요?

먼저 몇 개의 기호를 약정한다.

정의는 사칭 가등호로 "="를 표시합니다

표현식 전등은 두 개의 등호로 "=="를 나타낸다

귀약적 의미의 상등은 하나의 등호로'='를 나타내고,'=='는'='를 포함한다

lambda 연산은 기호를 정의할 수 없기 때문에 이러한 귀속 정의는 값을 구할 수 없습니다.

f := (lambda () (f))

어떻게 lambda 검산에서 귀속을 실현합니까?가장 간단한 귀속 함수부터 시작하다.깨우침이 있었으면 좋겠어요.

찾기\(\Omega\)

우선, 우리의 목표는 무한 순환하는lambda 표현식을 찾아내는 것이다.또한 이 표현식이 가장 짧을 것을 추가로 요구한다.
하나의 lambda 표현식은 세 가지 형식만 있을 수 있다.

기호(x, y,z 등),

함수(예를 들어 (lambda(x)x))),

응용(영문 응용 프로그램, 즉 함수 호출, 예를 들어 호출 함수func, 매개 변수 x 쓰기: (func x))..

1, 2가지 형식은 값(value)이라고도 부른다. 왜냐하면 그들은 귀약될 수 없기 때문이다.무한 순환 표현식은 세 번째 형식일 수 있습니다.

(exp1 exp2)

exp1을 고려하다.exp1은 함수이거나 함수로 요약될 수 있는 응용입니다.만약 exp1이 응용된다면, exp1은 함수에 귀약되거나 무한 순환될 것이다.만약 exp1이 무한 순환한다면 우리의 가장 짧은 가설과 모순되기 때문에 exp1은 하나의 함수로 귀약될 것이다.만약 exp1이 하나의 함수에 귀약된다면, exp1과 하나의 함수와 별 차이가 없다.간단하게 고려하여 exp1이 함수라고 가정합니다.

exp1 := (lambda (x) body)

그렇다면

(exp1 exp2)

== ((lambda (x) body) exp2)

=  body[x <- exp2]

표현식을 무한 순환시키기 위해서 우리는 다음과 같이 희망한다.

(exp1 exp2) == body[x <- exp2]

그래서 바디는 응용 프로그램일 거예요.

body := (subexp1 subexp2)

<=> (exp1 exp2) == (subexp1[x <- exp2] subexp2[x <- exp2])

<=> exp1 == subexp1[x <- exp2]  and  exp2 == subexp2[x <- exp2]

마지막 조건에서 제공 가능:

exp2 == subexp2[x <- exp2]  <=>  subexp2 == x

또한 표현식 exp1에는 exp2와 같은 하위 표현식이 포함되어 있음을 알 수 있다.이 조건을 충족시키는 가장 간단한 exp1은 exp2와 같은 exp1이다.

exp1 == exp2

<=> subexp1[x <- exp2] == exp2

<=> subexp1 == x

몇 가지 조건을 종합하면 다음과 같습니다.

exp1

== (lambda (x) body)

== (lambda (x) (subexp1 subexp2))

== (lambda (x) (x x))



exp2

== exp1

== (lambda (x) (x x))

그래서 우리가 찾는 무한순환의 표현식은 다음과 같다.

((lambda (x) (x x)) (lambda (x) (x x)))

이 표현식은 lambda 연산의\(\Omega\) 표현식입니다.\(\Omega\) 표현식 순환의 관건은 (f) 형식의 표현식, 즉 자신에게 적용하는 것입니다.\(\Omega\) 에는 세 가지 형식의 표현식이 포함되어 있습니다.

Y Combinator 찾기

일반적으로 귀속 함수는 이렇게 길다.

target := (lambda args body[target])

body[target]의 뜻은 target이라는 기호를 포함하는 표현식입니다. args는 이것은 임의의 개수 매개 변수의 함수입니다.이 표현식에서 target은 구속이 없는 기호입니다.무제약 기호를 포함하는 표현식은 값을 구할 수 없습니다.Lambda 연산에서 하나의 기호를 제약하는 방법은 lambda 키워드를 사용하는 것입니다. target을 제약 기호로 바꾸기 위해 우리는 표현식을 고칩니다.

p := (lambda (target)

       (lambda args body[target]))

   = (lambda (f)

       (lambda args body[f]))

혼동을 피하기 위해, 위에서 target을 f(\(\alpha\)귀약)로 개명하고, target은 우리가 원하는 귀속 함수의 표현식을 표시합니다.target과 p는 다음과 같은 관계가 있습니다.

(p target)

= (lambda args body[target])

= target

참고로 우리가 찾고 있는 target은 p의 부동점임을 알 수 있다.
다음은 target을 어떻게 찾을지 생각해 봅시다.\(\Omega\) 의 깨우침을 찾으시겠습니까?우리는 target이 (g) 형식의 표현식일 것이라고 추측한다.

target == (g g)

=>

  (p target) = target

  <=> (p (g g)) = (g g)

  <=> (g g) = (p (g g)) = ((lambda (x) (p (x x))) g)

마지막 조건에서 알 수 있듯이

g := (lambda (x) (p (x x)))

=>

  target == (g g)

  == ((lambda (x) (p (x x)))

        (lambda (x) (p (x x))))

p를 매개변수 위치로 추출하려면 다음과 같이 하십시오.

target = 

((lambda (f)

   ((lambda (x) (f (x x)))

    (lambda (x) (f (x x))))) p)



Y :=

(lambda (f)

  ((lambda (x) (f (x x)))

   (lambda (x) (f (x x)))))



target = (Y p)

이 Y가 바로 Y combinator입니다.

Y combinator를 사용하여 \(\Omega\)

가장 간단한 무한 순환 함수는 다음과 같다.

f := (lambda () (f))

Y combinator를 이용하여 이 함수의 lambda 표현식을 생성하면 무엇을 얻을 수 있습니까?

(Y (lambda (f) (lambda () (f))))

= ((lambda (x) ((lambda (f) (lambda () (f))) (x x)))

   (lambda (x) ((lambda (f) (lambda () (f))) (x x))))

= ((lambda (x) (lambda () ((x x))))

   (lambda (x) (lambda () ((x x)))))

휴, 이렇게 많은 괄호를 맞추는 것은 정말 쉽지 않다.참고(\(\eta\) 요약):

(lambda () ((x x))) = (x x)

그래서

(Y (lambda (f) (lambda () (f))))

= ((lambda (x) (x x)) (lambda (x) (x x)))