이전 주제 보기 :: 다음 주제 보기 |
글쓴이 |
메시지 |
이중호
가입: 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
가 되는게 아닐까 합니다 |
|
위로 |
|
|
허기홍
가입: 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알고리즘으로 풀면 되는데
그 설명은 위에 현철씨가 해주셨네요. |
|
위로 |
|
|
|