전화 걸기 평가를 오해하는 이유는 무엇입니까?

Question

우선, 이런 것들을 공부 한적이 없으므로 유감스럽게 생각하는 바보 같은 질문을 할 수도 있습니다. :)

나는 람다 계산을 구현하는 중입니다. , 필요에 따라 전화를받습니다. 나는 해당 비트가 28 페이지에 설명 된 자연스런 의미로 보이는 주제에 대해 this paper을 따르려고합니다.

어쨌든이 평가 전략에 대해 이해할 수없는 것은 이해할 수있는 한 실제 대체는 변수를 평가할 때만 발생합니다. 추상화는 값이기 때문에 자체적으로 평가되며 응용 프로그램은 캐시에 새 항목 만 추가합니다.

그러나, 하나

(λx.λy.x y) λa.a

링크 된 문서에 설명 된 자연의 의미에 따르면 같은 기간의 평가에 대해 정확히 어떻게 갈 주어진는 첫 번째 평가 단계에 진입 x -> λa.a를 추가하는 것입니다 캐시에 저장하고 응용 프로그램의 lhs에있는 추상화 본문 인 λy.x y을 평가합니다. 그러나 이것은 가치이므로 평가가 끝납니다. 어떤 시점에서 우리는 닫히지 않은 용어와 비어 있지 않은 힙을 가지고 있습니다. 이 용어의 정확도는 λy.(λa.a) y입니다.

내가 뭘 잘못 알고 있니? 이 평가 전략을 실제로 사용하는 언어에서는 어떻게 작동합니까?

Answer 1

귀하의 감소입니다. 요점은 그 논문에서 다루어 진 필요성에 의한 부름 전략은 람다 (lambda) 표현 하에서 결코 감소하지 않는다는 점에서 약한 전략 일뿐입니다. 이것은 그림 1에서 분명합니다. \ x.M 표현식은 값입니다.

람다 (rambda) 용어를 명시 적으로 얻고 싶다면 용어에서 캐시의 연관성을 대체 할 수있는 캐시를 풀어야합니다 (일반적으로 문헌의 환경이라고도 함).

   λy.x y [x -> λa.a] = λy.(λa.a) y 

예상대로