|
|
이전 주제 보기 :: 다음 주제 보기 |
글쓴이 |
메시지 |
유진선14
가입: 2018년 9월 11일 올린 글: 18
|
올려짐: 2018년12월11일 17:20 주제: 7-1 Var 질문 |
|
|
조교님 안녕하세요, 7-1을 풀던 중 뼈대코드의 내용에 질문이 생겨 글을 올리게 되었습니다.
M 알고리즘에서 Var의 경우 알고리즘을 보면
M(G, x, tau) = unify(tau, {Ai -> Bi} tau') 라고 되어있습니다.
1) 여기서 {Ai -> Bi} tau'의 의미를 "tau' 안에 있는 모든 for all Ai를 찾아 for all Ai를 Bi로 바꾸는 substitute를 실행한다"로 이해했습니다.
2) 그리고 그렇게 되면 Ai에 붙어있던 for all 이 떨어지므로 그 결과는 Simple Type이 된다고 이해했습니다.
이런 상황에서, 뼈대코드 subst_scheme에서 tyscm이 GenTyp일 때 SimpleTyp이 아닌 GenTyp (betas, subs (s' t))를 뱉어내는 이유가 궁금합니다. 여기에서 betas의 역할이 무엇인지 짐작이 가지 않습니다. 혹시 {Ai->Bi} tau'는 SimpleTyp라는 제 이해가 잘못된 것인가요?
답변에 항상 감사드립니다.
유진선 올림. |
|
위로 |
|
|
배요한 Site Admin
가입: 2018년 3월 6일 올린 글: 107
|
올려짐: 2018년12월11일 18:30 주제: |
|
|
안녕하세요, 유진선 학생.
1,2번 잘 이해하신게 맞습니다.
M(gamma, x, tau)는 알파들이 instantiate 되어 베타로 바뀌고 forall이 사라지게 되는 경우입니다.
반면, subst_scheme는 gamma에 대한 치환이 일어날 때 쓰는 함수입니다. 예를 들어, exp가 함수(\x.E)일 때, M에서는 다음과 같이 정의되어 있습니다.
코드: | S1 = unify(gamma, E1, ...)
S2 = M(S1 gamma + x : S1B1....)
in S2 ∘ S1 |
(S1 gamma + x) 처럼, 계산된 S1을 gamma에 적용해야 할 때 해당 함수가 사용됩니다.
이 때, GenTyp을 치환할때, GenTyp을 유지하되, 알파들에 대해서는 베타들로 alpha conversion 이 일어났다라고 보시면 됩니다.
TA 이동권
e-mail: dklee@ropas.snu.ac.kr
TA 배요한
e-mail: yhbae@ropas.snu.ac.kr |
|
위로 |
|
|
|
|
새로운 주제를 올릴 수 없습니다 답글을 올릴 수 없습니다 주제를 수정할 수 없습니다 올린 글을 삭제할 수 없습니다 투표를 할 수 없습니다
|
Powered by phpBB 2.0.21-7 (Debian) © 2001, 2005 phpBB Group Translated by kss & drssay
|