이전 주제 보기 :: 다음 주제 보기 |
글쓴이 |
메시지 |
이중호
가입: 2009년 9월 19일 올린 글: 35
|
올려짐: 2009년11월5일 18:13 주제: 알파 컨버젼 질문입니다 |
|
|
알파 컨버젼의 경우 정의가 x'이 FV(\x.e)의 원소가 아닐경우
\x.e -> \x'.{x'/x}e라고 되어 있습니다
그러면 베타 리덕션을 할때에 알파 컨버젼을 먼저 하고 해도 x'이 모두 사라지지 않나요?
김성준씨께서 올려주신 테스트셋의 결과를 보면 x!라는 것이 있던데 이게 알파컨버젼을 한 것 같은데
분명 베타 리덕션시에 (\x.e1) e2를 알파 컨버젼 하고 (\x!.e1) e2 이후 베타 리덕션을 하면 {e2/x!}e1이 되므로 결과에 x!은 나타나지 않아야 하는것 아닌지요 |
|
위로 |
|
|
허기홍
가입: 2007년 9월 27일 올린 글: 231
|
올려짐: 2009년11월5일 20:58 주제: |
|
|
알파 컨버전은 계산에 아무런 영향을 미치지 않습니다.
x!이 되었건 y, z가 되었건 상관없는 것이죠.
김성준씨가 어떻게 구현하셨는지 모르겠지만..
아래 예를 보시죠.
(\x\y. x y) y
여기서 알파컨버전을 하면
(\x\y!. x y!) y 이죠.
베타 리덕션을 하면
\y!. y y!
가 되어서 y!가 남습니다. |
|
위로 |
|
|
|