|
|
이전 주제 보기 :: 다음 주제 보기 |
글쓴이 |
메시지 |
한재호 손님
|
올려짐: 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 를 말하는 것이겠죠?
|
그렇습니다.
한재호 씀: |
그리고 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)가 되어 |
쓸데없이 질문의 본질과 관계없이 ,를 넣었다가 틀려버렸군요 `(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에 대해서 결과 값으로는 허용하지만, 어떤 연산을 취하는 것은 허용하지 않는 것과 같은 맥락에서 이해하시기 바랍니다.
@ 시그마 기호도 찾으시고 아래 화살표도 찾으시고, 멋지십니다. |
|
위로 |
|
|
안형찬
가입: 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 주제: |
|
|
결국 또 실수를 하고 말았습니다 하지만 이제 어떤 의미인지 잘 알겠습니다. 감사합니다. |
|
위로 |
|
|
이기석
가입: 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(코드) 일 경우만 정의가
돼있습니다. |
|
위로 |
|
|
|
|
새로운 주제를 올릴 수 없습니다 답글을 올릴 수 없습니다 주제를 수정할 수 없습니다 올린 글을 삭제할 수 없습니다 투표를 할 수 없습니다
|
Powered by phpBB 2.0.21-7 (Debian) © 2001, 2005 phpBB Group Translated by kss & drssay
|