그래서 나는 \x->\y->x에서 두 번째 x가 첫 번째 것에 바인딩되어 있음을 알고 있습니다. (틀 렸습니다. 제발 잘못되었습니다.) \x->\x->x 마지막 x는 중간에 바인딩되어 있습니다. 그러나 이것은 알파 등가성에 관해서는 차이가 있습니까? x -> x -> x alpha는 x -> y -> x와 동일합니까?
\x->\y->x에 해당하는 \x->\x->x 알파가 있습니까?
두 경우 용어 t1 및 t2 어떤 문맥 E[.], E[t1] 대해 다음, α- 동등하며 E[t2] 동일한 용어로 감소시킨다.
따라서 두 개의 용어가 있고 두 개의 다른 용어로 축소하는 컨텍스트를 찾으면 알파가 아닌 것으로 알고 있습니다. 여기
, 당신이 t1 = \x.\x.x 가지고 t2 = \x.\y.x, 두 개의 서로 다른 용어를 적용 컨텍스트, 예를 들어,을 v1 및 v2, 당신은이 :
t1 v1 v2 = (\x.\x.x) v1 v2 --> (\x.x) v2 --> v2
및
t2 v1 v2 = (\x.\y.x) v1 v2 --> (\y.v1) v2 --> v1
알파 등가성을 사용하여 실제로 작업하고 싶다면 자유 변수와 바운드 변수가 무엇인지 이해하고 변수 바인딩과 관련하여 알파 등가가되는 것이 무엇인지 스스로에게 질문해야합니다.
나는 결코 신경 쓰지 않기 위해 열심히 노력할 것입니다. * 이름을 다시 사용하지 마십시오. * – Caleth