게시판 인덱스

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

7-1 Var 질문

 
이 게시판은 잠겼으므로 글을 올리거나, 답변을 하거나 수정을 할 수 없습니다   이 주제는 잠겼으므로 답변을 하거나 수정을 할 수 없습니다     게시판 인덱스 -> 4190.310 Programming Languages (Fall 2018)
이전 주제 보기 :: 다음 주제 보기  
글쓴이 메시지
유진선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
위로
사용자 정보 보기 비밀 메시지 보내기
이전 글 표시:   
이 게시판은 잠겼으므로 글을 올리거나, 답변을 하거나 수정을 할 수 없습니다   이 주제는 잠겼으므로 답변을 하거나 수정을 할 수 없습니다     게시판 인덱스 -> 4190.310 Programming Languages (Fall 2018) 시간대: GMT + 9 시간(한국)
페이지 11

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


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