게시판 인덱스

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

TypeChecker 질문입니다

 
이 게시판은 잠겼으므로 글을 올리거나, 답변을 하거나 수정을 할 수 없습니다   이 주제는 잠겼으므로 답변을 하거나 수정을 할 수 없습니다     게시판 인덱스 -> 4190.310 Programming Languages (Fall 2009)
이전 주제 보기 :: 다음 주제 보기  
글쓴이 메시지
이중호



가입: 2009년 9월 19일
올린 글: 35

올리기올려짐: 2009년11월13일 19:50    주제: TypeChecker 질문입니다 인용과 함께 답변

어찌 해야되는지 전혀 감을 잡지 못해

듀가 지난 상황에서도 이러고 있습니다,,,

책에 나와있는 V알고리즘과 U알고리즘을 사용해서 만드는 것이 맞는건지

이경우 주어진 M definition의 타입체커 시만틱을 어떻게 적용해야 하는지

전혀 감이 오지 않습니다

let val x = 1 in
let f = fn x => x in
f x
end
end

가 들어오면 이러한 알고리즘을 어찌 적용하여 답을 내는지 설명좀 부탁드립니다....

그리고 책 166페이지에 보면
unify-all(u ^ u'; S) = let T = unify-all(u; S) in unify-all(Tu'; T)
여기서 Tu'은 무었인가요? T가 Subset이면 u'이 t여야 하는데 u'은 Equation아닌가요?
위로
사용자 정보 보기 비밀 메시지 보내기
현철



가입: 2009년 10월 7일
올린 글: 27

올리기올려짐: 2009년11월13일 20:37    주제: 인용과 함께 답변

제가 이해하기론

unify-all( a, b )의 의미는
현재 솔루션 셋 b에서 방정식 a가 추가되었을 때의 b에 덧붙여져 추가되는 솔루션 + b인데요.

let T = unify-all( u; S)
의 의미는 S solution을 이용해서 u를 풀어본다는 의미고..
unify-all( Tu'; T)는 T솔루션을 이용해서 u'을 일단 현재까지는 풀어진 솔루션으로 치환해본 뒤에 방정식을 푼다는 의미라고 생각합니다.

a0를 a1으로 치환하는 게 S이고
u = { a2 = a0 -> a1 }
u' = { a2 = int -> a0 }
이면

T는
{ a0 = a1, a2 = a1 -> a1 }이고

Tu'은
a2 = int -> a1

unify-all( Tu'; T )는
a0 = a1
a1 = int
a2 = int -> int

가 되는게 아닐까 합니다 Smile
위로
사용자 정보 보기 비밀 메시지 보내기
허기홍



가입: 2007년 9월 27일
올린 글: 231

올리기올려짐: 2009년11월14일 15:28    주제: 인용과 함께 답변

숙제 문서에 있는 타입 시맨틱은
정적 타입시스템을 수학적으로 정의한 것입니다.

그것을 알고리즘으로 구현한 것이 책에 있는 여러 알고리즘 입니다.
책에서 온라인/오프라인 알고리즘을 설명하고 있습니다.

오프라인을 궁금해하시는 것 같으니 이를 설명드리자면

코드:

let val x = 1 in
let f = fn x -> x in
f x


우선 V 알고리즘을 사용하여 연립방정식을 도출합니다.
163쪽을 보시면 알고리즘이 있죠.
책에 없는 부분은 학생들이 알아내는 것이 숙제이니 대략적으로 설명을 드리겠습니다.

프로그램의 타입은 맨 바깥 let x e1 e2 의 타입과 같고 그것은 e2의 타입과 같습니다.
첫번째 let x e1 e2 를 보시면
x가 정수 타입임을 알 수 있습니다.

그리고 e2에 대한 방정식을 세우는데 환경에 x는 정수 타입임을 기록해 둡니다.
두번째 let 을 보면
f가 a1 -> a2 타입임을 알수 있습니다.

f의 인자 x가 a1임을 환경에 기록한채로 f의 바디를 보면
f의 리턴값이 a1임을 알수 있습니다.(x를 리턴하므로)

f x 를 봅시다. f x는 이 프로그램의 최종 리턴 타입 t와 같습니다.
따라서 f 는 a3-> t 타입이고, a3의 타입은 x의 타입, 즉 int 입니다.

이 과정에서 나온 방정식으로 모두 ^ 로 묶은 것이 연립방정식입니다.

그것을 U알고리즘으로 풀면 되는데
그 설명은 위에 현철씨가 해주셨네요.
위로
사용자 정보 보기 비밀 메시지 보내기 이메일 보내기 글 올린이의 웹사이트 방문
이전 글 표시:   
이 게시판은 잠겼으므로 글을 올리거나, 답변을 하거나 수정을 할 수 없습니다   이 주제는 잠겼으므로 답변을 하거나 수정을 할 수 없습니다     게시판 인덱스 -> 4190.310 Programming Languages (Fall 2009) 시간대: GMT + 9 시간(한국)
페이지 11

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


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