@domatdo도막도
thunk . force
가 좀 난해한 녀석이죠. thunk
를 LISP의 quasi quotation으로, force
를 back quotation으로 이해하면 thunk . force
는 항등입니다만, thunk
를 그냥 지연된 계산으로 이해하면 thunk (M)
은 지연된 M
계산이고 thunk (force (thunk (M)))
은 지연된 force (thunk (M))
계산이라 같다고 하기 미묘합니다. 이 맥락에서 같다는 두 프로그램이 실행되어서 문법적으로 동일한 결과 값을 준다는 이야기일 때요.
@ailrunAilrun (UTC-5/-4) (force . thunk) m = m이라 볼 수 있지 않았나요?
If you have a fediverse account, you can reply to this note from your own instance. Search https://hackers.pub/ap/notes/01963f97-0bfc-7a45-b141-0b0ca1b2c8c6 on your instance and reply to it.
@ailrunAilrun (UTC-5/-4) 정확한 의미론을 보면 알 수 있겠네요. 아침에 일어나서 한 번 살펴봐야겠습니다 ㅎㅎ
@domatdo도막도 그 둘은 같습니다만
thunk
에 congruence rule이 없습니다. 즉 M = L
이어도 thunk(M) = thunk(L)
인 것은 아닙니다. (M
을 계산한 결과가 L
인 경우, thunk(M)
은 지연된 계산이기 때문에 더이상 평가가 진행되지 않아 thunk(L)
이 될 수 없습니다.)