[복진욱]

1.
\x.(x (\y.y))(\z.z)식은 제가 아는 한 더 이상 줄일 수 없으며
\x.(x)(\y.y)(\z.z)식은 뒤의 y람다와 z람다가 reduce될 수 있어 \x.(x)(\z.z)로 결과값이 나오는 걸로 알고 있습니다. 그러나 저 두 식을 ./run -pp하보면 완전이 일치하는
Lam (x,
App (
App (
Id x,
Lam (y,
Id y
)
),
Lam (z,
Id z
)
)
)
로 나오는데 reduce는 어떤 방향으로 해석해야 하나요?
아니면 제가 지금 람다식에 대하여 잘못 이해하고 있는 건가요?

2. 5-2번에서 숫자는 어떤 방식으로 표현해야 하나요? 수업시간에 배운대로 /n.z를 0으로 해석하듯이 하면 되나요?

[강동옥]

1.
질문하신 것은 reduce의 문제라기 보다 파싱 이슈입니다.

lambda x. a b c
가 있다면

((lambda x. a) b) c
lambda x. (a (b c))
lambda x. ((a b) c)

등 다양한 방식으로 associativity에 따라 파싱이 될수 있습니다.
파서의 구현에 따라
이중 한가지로 결정하게 되는데

저희가 제공한 파서에서는
lambda x. ((a b) c)
를 선택한것 뿐입니다.

의도한 테스트를 하기 위해서는
애초에 애매하지 않게 괄호를잘 쳐주면 됩니다.
예를 들어 lambda x. (x ((lambda y.y) (lambda z.z)))를 의도한거라면
\ x. (x ((\ y.y) (\ z.z)))라고 써보시면 의도한 pp를 얻을수 있을겁니다.

associativity가 애매한 코드는
pretty print를 한 기준으로 생각해주세요.

요약:
(1). 1+2+3은 (1+2)+3일수도 있고 1+(2+3)일수도 있으므로 파서는 한가지를 선택하게 됩니다.
(2). 따라서 저희 파서에서 두가지 코드는 모두 동일한 람다식입니다.
(3). 의도한대로 정확하게 쓰고싶다면 괄호를 열심히 치세요.



2.
인코딩은 어떤 방식이든 일관되면 됩니다. 0이 어떤때는 \n. z z인데 어떤때는 \n.z라면 문제겠지요. (물론 \x.x, \y.y와 같이 단지 naming차이는 동일한 것입니다.)