강동옥
가입: 2009년 9월 18일 올린 글: 602
|
올려짐: 2014년12월3일 14:17 주제: [답변정정]: 타입 추론 알고리즘 질문입니다. |
|
|
https://ropas.snu.ac.kr/phpbb/viewtopic.php?p=12772#12772
인용: | 교재 172쪽에 있는 completeness에 대한 설명에서,
감마' ㅏ e : tau' =>W(감마,e)=(tau,S) and (감마'=RS감마) and (tau'=R tau)
라고 나와있는데요,
알고리즘의 completeness를 증명하기 위해서는 위 식이 아니라
감마' ㅏ e : tau' =>W(감마,e)=(tau,S) and (감마'=RS감마) and (tau'=RS tau)
를 증명해야하지 않을까요? 강의자료와 교과서 모두 같은 식으로 설명되어있어 질문드립니다. |
교재에 나와있는 내용이 맞습니다.
S에는 각각의 alpha가 어떤 타입인가의 해를 담고 있게 됩니다.
그러므로 tau에 substitution S를 적용하는것은 무의미합니다. |
|