게시판 인덱스

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

K- Semantics 5페이지 Lift 관련 정의에서요

 
이 게시판은 잠겼으므로 글을 올리거나, 답변을 하거나 수정을 할 수 없습니다   이 주제는 잠겼으므로 답변을 하거나 수정을 할 수 없습니다     게시판 인덱스 -> 4190.310 Programming Languages (Fall 2005)
이전 주제 보기 :: 다음 주제 보기  
글쓴이 메시지
한재호
손님





올리기올려짐: 2005년10월27일 14:05    주제: K- Semantics 5페이지 Lift 관련 정의에서요 인용과 함께 답변

5번째줄 오른쪽에 Mㅏ, E||b, M1 이라고 되어 있는데
b 는 tf 를 말하는 것이겠죠?

그리고 6번째줄 분자 부분에
MㅏE||E1,M1 인데요
0 stage evaluation에서 E가 E1으로 갈 수가 있나요?
Mㅏ1E||E1, M1을 의미하신 것 아닌가요?
위로
안형찬



가입: 2005년 10월 22일
올린 글: 12

올리기올려짐: 2005년10월27일 17:55    주제: 인용과 함께 답변

저도 그 규칙이 궁금합니다.

저도 E가 '(E1)이라면 모를까 E1으로 평가될 수는 없다고 생각합니다. 그렇다고 ㅏ1을 생각하자면 다른 lift규칙에서 미루어 생각할 때 어색하므로, 굳이 끼워 맞추자면

σ,MㅏE↓'(E1),M1
──────────
σ,Mㅏlift(E)↓'(E1),M1

과 같이 정의할 수는 있을 것 같습니다만, 이래서는 lift()가 아무런 일도 하지 않게 하는 정의가 되니 어색하긴 마찬가지입니다. 주어진 semantics를 떠나 생각해보아도, lift안의 식을 평가하여 얻을 수 있는 type들 중 정수와 bool외에 깔끔한 정의를 만들어 낼 만한 것이 무엇인지 짐작가지 않습니다.
위로
사용자 정보 보기 비밀 메시지 보내기
안형찬



가입: 2005년 10월 22일
올린 글: 12

올리기올려짐: 2005년10월27일 18:32    주제: 인용과 함께 답변

질문이 모호한 것 같아 덧붙입니다.

제가 적은 추론 규칙

σ,MㅏE↓'(E1),M1
──────────
σ,Mㅏlift(E)↓'(E1),M1

에 관해서는, 아래쪽의 질문에 대한 답변에서 ㅏ1이 아니라고 확인해 주셨고, 식도 값이라는 지적 등을 하신 것으로 보아 이렇게 하는 것이 옳다고 생각하였습니다. 원래 주어진 정의의 σ,MㅏE↓E1,M1 은 stage0에서의 평가 결과로 `()로 둘러싸이지 않은 식이 나타나는 추론규칙이 없기 때문에 E1이 나올 수는 없으며, 따라서 이는 `(E1)의 오타라고 생각했기 때문입니다.

그러나, 그렇다면 `(3+,(x+1))과 lift(`(3+,(x+1)))가 x의 값이 4일 때 공히
`(3+5)가 되어 lift()의 의미가 (괄호 내부가 식으로 평가될 때는) 없어지는 것이 아닌가 생각됩니다. 그래서 그것이 원래의 의도인지, 아니면 제가 위에서 멋대로 추정한 추론규칙이 잘못된 것인지 질문드립니다.
위로
사용자 정보 보기 비밀 메시지 보내기
김덕환



가입: 2005년 8월 29일
올린 글: 190

올리기올려짐: 2005년10월27일 19:01    주제: Re: K- Semantics 5페이지 Lift 관련 정의에서요 인용과 함께 답변

한재호 씀:

5번째줄 오른쪽에 Mㅏ, E||b, M1 이라고 되어 있는데
b 는 tf 를 말하는 것이겠죠?

그렇습니다. Embarassed

한재호 씀:

그리고 6번째줄 분자 부분에
MㅏE||E1,M1 인데요
0 stage evaluation에서 E가 E1으로 갈 수가 있나요?

당연히 갈 수 있습니다. 코드도 훌륭한 값입니다.

한재호 씀:

Mㅏ1E||E1, M1을 의미하신 것 아닌가요?

아닙니다. 문서에 적혀있는 그대로입니다.
위로
사용자 정보 보기 비밀 메시지 보내기
안형찬



가입: 2005년 10월 22일
올린 글: 12

올리기올려짐: 2005년10월27일 19:37    주제: 인용과 함께 답변

제 글에 잘못이 있었습니다. 죄송합니다.
인용:
그러나, 그렇다면 `(3+,(x+1))과 lift(`(3+,(x+1)))가 x의 값이 4일 때 공히 `(3+5)가 되어

쓸데없이 질문의 본질과 관계없이 ,를 넣었다가 틀려버렸군요 Embarassed `(3+,(lift(x+1)))과 lift(`(3+,(lift(x+1))))로 하였어야 합니다만, 또 틀릴까봐 걱정되니 단순히:

1. `(1+2)와 lift(`(1+2))가 같은 것이 아닌지요?


하나만 더 여쭈어 보겠습니다.

인용:
당연히 갈 수 있습니다. 코드도 훌륭한 값입니다.

아직 제 질문에는 답을 하신 것이 아닌데 한재호 님 질문의 답변만을 보고 앞서가는 것은 아닌지 걱정됩니다만.. 우선 말씀드리면,

2. 코드가 값이라는 것은 이해하고(?) 있습니다만, stage 0에서 "compute"되는 값은 주어진 규칙에 따르면 항상 `(E1)의 형태를 갖고 있는 것이 아닙니까? 제가 뭔가 헷갈리고 있는 것이라면, 실제로 이 규칙이 적용될 수 있는 간단한 staged K- 코드 조각을 적어주셨으면 좋겠습니다.
위로
사용자 정보 보기 비밀 메시지 보내기
김덕환



가입: 2005년 8월 29일
올린 글: 190

올리기올려짐: 2005년10월27일 19:40    주제: 인용과 함께 답변

안형찬 씀:

원래 주어진 정의의 σ,MㅏE↓E1,M1 은 stage0에서의 평가 결과로 `()로 둘러싸이지 않은 식이 나타나는 추론규칙이 없기 때문에 E1이 나올 수는 없으며, 따라서 이는 `(E1)의 오타라고 생각했기 때문입니다.

`()로 둘러싸인 식만 결과값으로 나온다는 것은 맞습니다만, E1이 임의의 수식을 의미할 수 있으므로 그런 경우를 포함한다는 것을 간과하셨습니다.

형찬 님 수식의 형태로 표현하자면 다음과 같습니다.

σ,MㅏE↓`(E1),M1
──────────
σ,Mㅏlift(E)↓`(`(E1)),M1

그러면, `(`(E)1)이 등장해서 의아해하시겠지만, 결과 값으로 그런 수식이 등장하는 것은 허용합니다. 단지 그 값에 어떤 연산을 취하게 되면 에러가 발생하게 되는 것이지요. Bot에 대해서 결과 값으로는 허용하지만, 어떤 연산을 취하는 것은 허용하지 않는 것과 같은 맥락에서 이해하시기 바랍니다.

@ 시그마 기호도 찾으시고 아래 화살표도 찾으시고, 멋지십니다. Smile
위로
사용자 정보 보기 비밀 메시지 보내기
안형찬



가입: 2005년 10월 22일
올린 글: 12

올리기올려짐: 2005년10월27일 19:57    주제: 인용과 함께 답변

인용:
E1이 임의의 수식을 의미할 수 있으므로 그런 경우를 포함한다는 것을 간과하셨습니다.


아, 그러고 보니 그렇네요.; `()를 '식인 값'을 추론 규칙에서 자연스럽게 드러내기 위한 표기상의 장치로 생각했습니다만, 꼭 그렇게 볼 이유는 없었군요.
그렇다면, 제가 맞게 이해했는지 두가지만 확인 드리겠습니다.

1.
인용:
`()로 둘러싸인 식만 결과값으로 나온다는 것은 맞습니다만,

이므로, 주어진 스펙의 그 규칙을

σ,MㅏE↓`(E1),M1
──────────
σ,Mㅏlift(E)↓`(`(E1)),M1

이것으로 바꾸어도 두 semantics는 완전히 동등하다.

2.
eval(lift(`(1+2)))
의 semantics는 정의되지 않는다.(에러이다)

두 가지 다 맞습니까?
위로
사용자 정보 보기 비밀 메시지 보내기
김덕환



가입: 2005년 8월 29일
올린 글: 190

올리기올려짐: 2005년10월27일 20:41    주제: 인용과 함께 답변

안형찬 씀:

주어진 스펙의 그 규칙을

σ,MㅏE↓`(E1),M1
──────────
σ,Mㅏlift(E)↓`(`(E1)),M1

이것으로 바꾸어도 두 semantics는 완전히 동등하다.

현재 정의에서는 그렇습니다.
안형찬 씀:

eval(lift(`(1+2)))
의 semantics는 정의되지 않는다.(에러이다)

그렇지 않습니다. eval의 정의를 보면 중간 계산 과정에서 `(`(1 + 2))가 나오자마자 `()를 한꺼풀 벗깁니다. 따라서, `(`(1 + 2))에 연산이 적용되지 않으며(stage가 2로 올라가지 않으며), 최종적으로 에러가 발생하지 않습니다.

의미가 정의되지 않는 지는 의미 정의를 따라 의미 트리를 생성해보시면 쉽게 아실 수 있습니다.
위로
사용자 정보 보기 비밀 메시지 보내기
한재호



가입: 2005년 10월 27일
올린 글: 14

올리기올려짐: 2005년10월27일 21:12    주제: 인용과 함께 답변

죄송하지만 아직도 의미를 모르겠습니다.

lift(1+2) -> `(3)
lift(not false) -> `(true)
가 된다는 것은 알겠는데...

lift({ x:= 0, y := 0}) 의 결과가 무엇인지 알려주실 수 있나요?
그것이 `({ x:= 0, y := 0}) 라면 QUOTE와 완전히 같은 것일 테고
뭔가 다를 것일 텐데, 모르겠습니다.
위로
사용자 정보 보기 비밀 메시지 보내기
안형찬



가입: 2005년 10월 22일
올린 글: 12

올리기올려짐: 2005년10월27일 21:16    주제: 인용과 함께 답변

결국 또 실수를 하고 말았습니다 Embarassed 하지만 이제 어떤 의미인지 잘 알겠습니다. 감사합니다.
위로
사용자 정보 보기 비밀 메시지 보내기
이기석



가입: 2005년 10월 3일
올린 글: 33

올리기올려짐: 2005년10월28일 0:40    주제: 인용과 함께 답변

한재호 씀:
lift({ x:= 0, y := 0}) 의 결과가 무엇인지 알려주실 수 있나요?
그것이 `({ x:= 0, y := 0}) 라면 QUOTE와 완전히 같은 것일 테고
뭔가 다를 것일 텐데, 모르겠습니다.

위의 경우는 sematic에 정의가 안 되어있는 경우 같은데요.
lift(e) 에서 e를 계산한 결과값이 N, B, E(코드) 일 경우만 정의가
돼있습니다.
위로
사용자 정보 보기 비밀 메시지 보내기 MSN 메신저
이전 글 표시:   
이 게시판은 잠겼으므로 글을 올리거나, 답변을 하거나 수정을 할 수 없습니다   이 주제는 잠겼으므로 답변을 하거나 수정을 할 수 없습니다     게시판 인덱스 -> 4190.310 Programming Languages (Fall 2005) 시간대: GMT + 9 시간(한국)
페이지 11

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


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