|
|
이전 주제 보기 :: 다음 주제 보기 |
글쓴이 |
메시지 |
장민석
가입: 2006년 9월 5일 올린 글: 165
|
올려짐: 2006년11월7일 0:27 주제: SuppS가 무엇인지요? |
|
|
강의 노트 관련 질문입니다.
오늘 배운 람다 칼큘러스 관련 강의 노트 4번째 장(그러니까 4-4라고 적혀있는 페이지)을 보면 다음과 같은 substitution 식이 있습니다.
코드: | S(入x.e) = 入x'.S{x'/x}e
where x' !∈ u {FV(e) | e/x ∈ S}
u SuppS
u FV(e) \ {x} |
여기서 몇 가지 기호의 의미를 모르겠습니다.
1. SuppS는 무엇인가요?
2. u는 무엇인가요? |
|
위로 |
|
|
박대준
가입: 2005년 10월 7일 올린 글: 245
|
올려짐: 2006년11월7일 14:47 주제: |
|
|
S = {e1/x1, e2/x2, ... , en/xn} 이라고 했을 때,
Supp(S)는 "support set of S"라는 의미로써, substitutee 변수들의 집합인 {x1, ... , xn}를 나타냅니다.
S를 변수에서 식으로 가는(Var -> Exp) 부분 함수(partial function)라고 생각한다면, S의 정의역이 바로 Supp(S)를 의미한다고 할 수 있습니다.
또한, 언급하신 식에서 3번 나타나는 u는 합집합 기호입니다.
이 때, 두번째 u와 세번째 u는 일반 합집합 기호이지만,
첫번째 U는 일반 합집합 기호를 다음과 같이 약간 확장한 것입니다.
코드: | s1,...,sn을 각각 임의의 집합이라고 했을 때:
U{s1,...,sn} = s1 u s2 u ... u sn |
강의 슬라이드에 있는 예제들과 substitution의 의미를 잘 생각해보신다면,
언급하신 식의 의미
이광근 씀: | 이미 묶여있는 놈은 건들지 않는다.
새롭게 묶이는 놈이 없도록 한다. |
를 쉽게 이해하실 수 있을 것이라고 생각합니다. |
|
위로 |
|
|
장민석
가입: 2006년 9월 5일 올린 글: 165
|
올려짐: 2006년11월7일 16:22 주제: |
|
|
답변에 감사드립니다.
추가적으로 몇 가지 질문드릴 것이 있습니다.
코드: | S(入x.e) = 入x'.S{x'/x}e --치환식 0
where x' !∈ u {FV(e) | e/x ∈ S} --조건 1
u SuppS -- 조건 2
u FV(e) \ {x} --조건 3 |
질문A. 조건 1은 substitution시 일반적인 substitutor e 내부의 자유 변수들이 (unique name으로 x'을 도입함으로 인해) 새롭게 묶이지 않도록 하기 위한 조건이지요?
질문B. 조건 2는 substitution시 이미 묶여있는 변수들을 건드리지 않기 위한 조건이지요?
질문C. 조건 3은 e의 자유 변수들이 새롭게 묶이지 않도록 하기 위한 조건이지요?
질문D. 조건 1의 x, e와 치환식 0의 x, e는 그 의미가 다른 것이지요? 제 생각엔 조건 3의 x, e는 치환식 0의 x, e와 의미가 동일한 반면, 조건 1의 x, e는 그와 무관한 일반적 의미로 사용된 것 같습니다.
제가 제대로 이해하고 있는 건지 모르겠네요.;; |
|
위로 |
|
|
박대준
가입: 2005년 10월 7일 올린 글: 245
|
올려짐: 2006년11월8일 16:32 주제: |
|
|
제가 장민석님의 질문을 제대로 이해했다면, 맞습니다. |
|
위로 |
|
|
|
|
새로운 주제를 올릴 수 없습니다 답글을 올릴 수 없습니다 주제를 수정할 수 없습니다 올린 글을 삭제할 수 없습니다 투표를 할 수 없습니다
|
Powered by phpBB 2.0.21-7 (Debian) © 2001, 2005 phpBB Group Translated by kss & drssay
|