[박광석]

5-1 질문

1. reduction 구현을 할 때 eager-evaluation / lazy-evaluation 중 어떤 방식으로 할 것인지는 상관이 없는건가요?

2. (\x.(x x)) (\x.(x x))와 같은 식은 무한루프를 도는게 정상인가요?


5-2 질문

1. 과제가 요구하는 최종 출력은 reduction이 되지 않은 lambda코드인가요? reduction된 normal term인가요? (제가 숙제의 요구사항을 잘 이해하지 못하고 있는 것 같습니다. 앞서 질문 5번의 답변을 보면 변환만 하는 것 같은데 맞나요?)

[안준환]

5-1.

1. 문제에 보면 normal-order reduction rule을 따르도록 하라고 되어 있습니다. normal-order reduction은 항상 가장 왼쪽의 가장 바깥쪽 redex부터 reduce하기 때문에 lazy evaluation이 됩니다.
예를 들어 (\x.\y.x) ((\x.x) a) ((\x.x) b)를 normal order로 reduction하면 다음과 같습니다.

여기서 (\x.x b) 부분이 evaluation되지 않는 것을 볼 수 있습니다. eager evaluation을 사용한다면 다음과 같이 되어야 할 것입니다.


2. 네. 말씀하신 식을 normal-order로 한 번 reduction하면 여전히 (\x.(x x)) (\x.(x x))이므로 프로그램은 종료되지 않을 것입니다. reduction이 evaluation에 대응된다는 사실을 생각하면 정상적인 결과입니다.

5-2.

1. reduce되지 않은 lambda 식입니다. 이 문제는 M0 언어로 짜여진 프로그램을 lambda 식으로 번역하는 번역기를 작성하는 것이 목적이기 때문에 reduction, 즉 evaluation을 번역기가 수행하는 것은 의미에 맞지 않습니다.

2. 물론 하나의 프로그램에 대해 번역 결과는 여러 가지가 있을 수 있습니다. 하지만 문제에서 항상 끝나는 프로그램에 한정했으므로 Church-Rosser Theorem에 의해 동일한 encoding을 사용했다면 reduction 결과는 동일할 것입니다. 마치 이전 숙제에서 작성한 K-- 번역기를 테스트할 때 번역된 프로그램을 실행시킨 후 결과값을 비교하는 것과 유사하다고 생각하시면 될 것 같습니다.

3. M0에서 boolean이 필요할 것 같은 부분은 ifzero 뿐인데 만약 AND 수행 결과가 true에 해당하는 \x.\y.x라면 ifzero를 수행할 때 문제가 될 것입니다. 자연수 1 또는 0에 해당하는 값이어야 맞을 것 같습니다.

---------

혹시 답변에 잘못된 점이 있으면 조교님이나 다른 분들께서 지적해 주시면 감사하겠습니다.