[방정호]

5-1 에서 LETF, CALLV 관련 질문입니다.
재귀함수를 처리하려고 할 때, K-의 semantic은 CALLV 할 때 fenv에 추가를 하는 방식으로 되는데요.

sm5 에서는 call 시에 Env가 바뀌어버리고, 그 바뀐 env를 수정할 방법이 없는 것 같습니다.
이 작업을 미리 LETF를 처리할 때 해두는 방법 외에는 상상이 잘 안되는데, 이렇게 하면 K- 의 semantic과는 차이가 생기는 것 같습니다.

K- 의 semantic 이나 작업 순서와 달라도 상관이 없는 것인지 궁금합니다. (함수 정의 및 함수 호출과 관련)
그리고 혹시 제가 간과하고 있는 부분이 있어서 CALLV 처리를 헤매는 것이라면, 어느 부분을 보아야 할지 가이드를 주시면 감사하겠습니다.

[강동옥]

숙제 5 스펙 추가사항을 정리한 https://ropas.snu.ac.kr/phpbb/viewtopic.php?t=4532 글의 다음 부분이 질문하신 부분에 대한 답변이 될 것 같습니다.

[방정호]

같은 일을 한다와 관련되어 다른 질문 드리고 싶습니다.

과제 pdf 문서에서는
push 1::push 2::add::put::empty
이것이
write 1+2
가 같은 일을 한다고 나와있는데요.

k-의 write e 의 semantic은
e의 값을 계산해서 v 이면 v를 출력하고, 다시 v를 리턴한다고 되어있습니다. unit 등을 리턴하는 게 아니라 값을 리턴합니다.
예를 들어, (write 1) + 2 같은 일이 벌어질 경우 3이 남아야 하는게 k- semantic과 맞는 것 같고요.
그런데 sm5의 put은 stack의 머리에 z 가 있으면 그걸 출력하고 그 z를 없애버립니다. 즉 저 cmd list가 수행되고 나면 stack에 3이 남아있지 않고 빈 스택이 될텐데요.
그러면 write 함수가 v를 리턴하는 형태로 만드는 게 이 과제의 목적이 맞는지 의심이 가서요. 생각보다 많이 복잡해지네요.
과제 pdf 문서를 보면 상식 수준에서만 설명이 되어있어, 저렇게만 생각을 하고 구현을 해도 되는 것인지요?

SEQ 처리를 간단히 생각하고 만들다가 문제가 생겨서 살펴보다 보니 SEQ에서 추가 처리가 필요했는데요. 이럴 경우 write도 수정이 필요할 것 같았습니다. v를 출력하도록이요.
이런 이상한 케이스를 고려해야 하는 것인지 궁금합니다.

+
assign 에서도 비슷한 상황이 생기는 것 같습니다.

[강동옥]

음.. 여전히 질문하신 사항들에 대한 답은 "같은 일을 하는" 것에 대한 정의에 나와 있는 것 같습니다.

push 1::push 2::add::put::empty
는
write 1+2
와 같은 일을 합니다. 둘 다 초기 조건에서 시작했을 때 "3\n"을 출력하는 같은 side-effect를 가지고 있기 때문에, "같은 일을 한다"의 정의를 만족하기 때문입니다. 위의 프로그램은 실행되고 나서 스택이 비어있고, 아래의 프로그램은 최종적으로 3을 리턴하는 것은 같은 일을 한다는 조건과는 무관합니다. 스택에 3이 그대로 들어있어도 되고, 극단적으로 임의의 정수가 수십개씩 쌓여있어도 "같은 일을 한다"는 조건은 만족합니다.

다른 예로, 만약 write ((write 1) + 2) 라는 K- 프로그램이 있다면 이는 k- semantics에 따라 "1\n3\n"을 출력해야 할 것입니다. 따라서, 이를 번역한 SM5 프로그램도 "1\n3\n"을 출력해야 하며, 그 조건만 만족한다면 그 과정에서 혹은 최종적으로 스택이 어떤 상태이건 무방합니다.

구체적으로 어떤 SM5의 명령들로 번역해야 하는지에 대해서 정보를 드리는 것은, 숙제의 구현과 관련된 문제이므로 답변을 드리기 힘들 것 같습니다.

[방정호]

답변 감사드립니다. 많은 궁금증이 풀렸습니다.