나는이 주제가 여러 번 논의되었다는 것을 알고 있지만 여전히 분명하지 않은 것이 있습니다. 나는이 질문 적용 순서 / 값별 호출 및 정상 주문 / 이름 별 호출 차이점을 읽었으며 한 번에 모두 명확히해야 할 것이 있습니다.
이름으로 전화
정상적인 순서이지만 추상화 내에서는 축소가 수행되지 않습니다. 예를 들어 λx. (λx.x) x는 redex (λx.x) x를 포함하지만이 전략에 따라 정규 형식입니다.
이름으로 호출 할 때 λx. (λx.x) x라는 표현은 정규 형식이라고합니다. 이것은 "(λx.x) x"가 몸체로 간주되기 때문입니까 (λ의 범위가 가능한 한 오른쪽으로 확장되기 때문에)? 그래서 반대편에 제가 정상적인 순서를 적용하면 어떤 결과가 나올까요?
이름으로 호출 할 때 λx. (λx.x) x라는 표현은 정규 형식이라고합니다. 이것은 "(λx.x) x"가 몸체로 간주되기 때문입니까 (λ의 범위가 가능한 한 오른쪽으로 확장되기 때문에)?
그래 당신 말이 맞아요.
그래서 반대편에 제가 정상적인 순서를 적용하면 어떤 결과가 나올까요?
body :를 축소 (λx.x)x -> x하면 모든 것이 identity 함수로 축소됩니다.
λx.(λx.x)x -> λx.x
더 나아가 조금을 명확히하기 위해, 내가이 한 번 더하자 이름을 변경 을 준수하기 위해 변수를 Barendregt 변수 규칙 : λx.(λx.x)x =α λx.(λy.y)x:
λx.(λy.y)x -> λx.[y := x](y) = λx.x
이 기사는 인터넷에서 수집됩니다. 재 인쇄 할 때 출처를 알려주십시오.
침해가 발생한 경우 연락 주시기 바랍니다[email protected] 삭제
몇 마디 만하겠습니다