게시판 인덱스

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

챌린지 1번에 관한 질문입니다.

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



가입: 2013년 9월 4일
올린 글: 26

올리기올려짐: 2014년11월25일 21:16    주제: 챌린지 1번에 관한 질문입니다. 인용과 함께 답변

1. type의 귀납적 정의를 x(변수), \x.e, e e, 그리고 상수 네가지로 한정해도 되나요?

2. 혹시나 하여 여쭙습니다만, 표현의 길이를 유한하다고 가정해도 되겠지요?

3. 최종적인 표현에 free variable이 존재할 수 있나요?

4. progress 정리의 '값이 나올 때까지 진행한다'라는 문장에서,
'값이 나온다'를 표현을 더 'reduce할 곳이 없음'으로,
'진행'을 reduction으로 이해해도 되나요?
다시 말해, 주어진 타입 시스템이 결과를 낸 프로그램들은 반드시 유한한 시간 내에 reduction이 불가능해지는 시점이 온다라고 이해해도 되나요?

만약 그렇다면, 타입 시스템이 Y combinator 같은 case를 처리하기 위해서는(no를 대답하거나/유한 시간 안에 yes를 뱉지 않음), e1 e2에 대한 ppt의 증명이 불충분하지 않나요? ppt는 e1, e2가 모두 값이라면, e1이 반드시 \x.e'의 꼴을 가져야 하기 때문에 {e2/x} e'으로 진행한다는 내용만을 포함하고 있습니다. 그러나 완전한 증명을 하기 위해서는 {e2/x} e'역시 최종적으로 값을 냄/귀납가정에 포함됨을 증명해야 하지 않을까요?

만약 위의 경우가 아니어서 타입 시스템이 \x.(x x)같은 경우를 걸러내지 못하거나, 혹은 progress 정리가 그저 'reduce할 곳이 남아있다면 reduce함'을 의미한다면 progress 정리의 의미가 무엇인가요?

5. 전체 증명의 과정에서 등장하는 귀납 가정을 구체적으로 정의하는 것 역시 과제의 일부인가요?

감사합니다.
위로
사용자 정보 보기 비밀 메시지 보내기
김성학



가입: 2013년 9월 4일
올린 글: 26

올리기올려짐: 2014년11월25일 21:25    주제: 인용과 함께 답변

위 '\.x (x x)' 부분은 잘못 작성했는데 Y combinator와 같이 스스로 적용하여 무한히 계속되는 케이스를 말하고자 한 것입니다 ㅜ
위로
사용자 정보 보기 비밀 메시지 보내기
김성학



가입: 2013년 9월 4일
올린 글: 26

올리기올려짐: 2014년11월27일 10:45    주제: 인용과 함께 답변

4,5번이 해결되었습니다! Smile
위로
사용자 정보 보기 비밀 메시지 보내기
강동옥



가입: 2009년 9월 18일
올린 글: 602

올리기올려짐: 2014년11월27일 12:17    주제: 인용과 함께 답변

1. e-> n |x |\x.e | e e| e+e로 하겠습니다.
value v-> n | \x.e

2. 네 유한합니다.

3. e는 free variable을 포함하지 않습니다.

4. 의미에 대해 말로 풀어서 설명드리면
(1)progress는 타입에 맞는 표현식은 (error가 아닌)value가 되거나 진행한다(reduce)는 의미입니다.
(2) preservation은 진행전 타입과 진행 후 타입이 같다는 뜻입니다.

progress후 value가 되는것이 필수는 아닙니다. 단지 멈춘다면 그것은 value이어야 한다는 의미입니다.

5. 증명하고자 하는 명제가 곧 귀납 가정이 되기 때문에 구체적으로 정의하지 않을수 없습니다.
위로
사용자 정보 보기 비밀 메시지 보내기
강혜진



가입: 2013년 9월 23일
올린 글: 6

올리기올려짐: 2014년12월19일 5:31    주제: challenge 1번 질문입니다 인용과 함께 답변

강동옥 씀:
1. e-> n |x |\x.e | e e| e+e로 하겠습니다.
value v-> n | \x.e

2. 네 유한합니다.

3. e는 free variable을 포함하지 않습니다.



progress / subjective reduction theorem에서, e = x인 경우 ㅏx : tau 를 증명할 때 타입 환경이 비어있으므로 x는 free variable입니다. e는 free variable을 포함하지 않는다고 하셨는데 그렇다면 progress / subjective reduction theorem의 경우 e = x인 경우는 증명하지 않아도 되나요?


또한,
(감마)ㅏE1:(이오타) (감마)ㅏE2:(이오타)
--------------------------------------------
(감마)ㅏE1+E2:(이오타)

라고 수정하셨는데 그렇다면 E = E1+E2의 경우 ㅏE:(tau) 일때 tau = iota가 되어 E는 항상 값인가요?
위로
사용자 정보 보기 비밀 메시지 보내기
강동옥



가입: 2009년 9월 18일
올린 글: 602

올리기올려짐: 2014년12월19일 14:55    주제: 인용과 함께 답변

감마가 비어있을경우 x에 대한 증명은 x가 freevariable이므로 필요 없겠지요.

하지만 실재 증명할때는 빈 감마를 써서는 증명이 안될겁니다. 그러므로 e=x인 케이스도 감마를 보면서 freevariable인지 여부를 봐야지요.


두번째 질문은 값이냐는 의미가 무슨의미인지 잘 모르겠습니다.
아직 e+e인 상태는 아직 값이 아닙니다.
타입체크가 되었다면 evaluation후에 값이 되겠지요.
위로
사용자 정보 보기 비밀 메시지 보내기
이전 글 표시:   
글 쓰기   답변 달기     게시판 인덱스 -> 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