게시판 인덱스

 
 FAQFAQ   검색검색   멤버리스트멤버리스트   사용자 그룹사용자 그룹   사용자 등록하기사용자 등록하기 
 개인 정보개인 정보   비공개 메시지를 확인하려면 로그인하십시오비공개 메시지를 확인하려면 로그인하십시오   로그인로그인 

타입 추론 알고리즘 질문입니다.

 
글 쓰기   답변 달기     게시판 인덱스 -> 4190.310 Programming Languages (Fall 2014)
이전 주제 보기 :: 다음 주제 보기  
글쓴이 메시지
정태호



가입: 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    주제: 인용과 함께 답변

아무리 생각해도 이상해서 다시 들어와보니 수정답변이 있네요ㅎㅎ

감사합니다!
위로
사용자 정보 보기 비밀 메시지 보내기
이전 글 표시:   
글 쓰기   답변 달기     게시판 인덱스 -> 4190.310 Programming Languages (Fall 2014) 시간대: GMT + 9 시간(한국)
페이지 11

 
건너뛰기:  
새로운 주제를 올릴 수 없습니다
답글을 올릴 수 없습니다
주제를 수정할 수 없습니다
올린 글을 삭제할 수 없습니다
투표를 할 수 없습니다


Powered by phpBB 2.0.21-7 (Debian) © 2001, 2005 phpBB Group
Translated by kss & drssay