이전 주제 보기 :: 다음 주제 보기 |
글쓴이 |
메시지 |
정태호
가입: 2014년 9월 11일 올린 글: 17
|
올려짐: 2014년12월2일 23:03 주제: 타입 추론 알고리즘 질문입니다. |
|
|
교재 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)
를 증명해야하지 않을까요? 강의자료와 교과서 모두 같은 식으로 설명되어있어 질문드립니다. |
|
위로 |
|
|
강동옥
가입: 2009년 9월 18일 올린 글: 602
|
올려짐: 2014년12월3일 0:05 주제: |
|
|
안녕하세요,
말씀하신 교재 내용을 확인해 보았습니다.
조교팀이 보기에도, 말씀하신 대로 아래와 같이 되는 것이 맞아 보입니다.
<img align="middle" src="http://ropas.snu.ac.kr/cgi-bin/mimetex.cgi?\Gamma'%20\vdash%20e%20:%20\tau'%20\Rightarrow%20W(\Gamma,e)=(\tau,%20S)%20\wedge%20(\Gamma%20'%20=%20RS%20\Gamm)%20\wedge%20(\tau'%20=%20RS%20\tau)"/>
교재 171쪽에 있는, "M 알고리즘이 타입 시스템의 충실한 구현"을 표현하는 수식에도 이와 비슷한 형식으로 표현되어 있는 것으로 보아 맞는 것 같습니다.
강동옥 가 2014년12월3일 14:10에 수정함, 총 1 번 수정됨 |
|
위로 |
|
|
정태호
가입: 2014년 9월 11일 올린 글: 17
|
올려짐: 2014년12월3일 8:20 주제: |
|
|
답변 감사합니다! |
|
위로 |
|
|
강동옥
가입: 2009년 9월 18일 올린 글: 602
|
올려짐: 2014년12월3일 14:15 주제: |
|
|
착각을 했습니다. 죄송합니다.
교재에 나와있는 내용이 맞습니다.
S에는 각각의 alpha가 어떤 타입인가의 해를 담고 있게 됩니다.
그러므로 tau에 substitution S를 적용하는것은 무의미합니다. |
|
위로 |
|
|
정태호
가입: 2014년 9월 11일 올린 글: 17
|
올려짐: 2014년12월3일 15:40 주제: |
|
|
아무리 생각해도 이상해서 다시 들어와보니 수정답변이 있네요ㅎㅎ
감사합니다! |
|
위로 |
|
|
|