이전 주제 보기 :: 다음 주제 보기 |
글쓴이 |
메시지 |
김성학
가입: 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번이 해결되었습니다! |
|
위로 |
|
|
강동옥
가입: 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후에 값이 되겠지요. |
|
위로 |
|
|
|