허기홍
가입: 2007년 9월 27일 올린 글: 231
|
올려짐: 2007년12월4일 17:25 주제: 숙제7의 질문입니다 |
|
|
S를 타입스킴 시그마에 적용하는 경우를 보면
인용: | S시그마 = 모든베타벡터.S{알파벡터 -> 베타벡터}타우 |
라고 되어있습니다.
제가 해석하기에 타우에 있는 알파벡터의 요소들이 나오면 모두 베타 벡터로 변형하고
그 바뀐 타우를 S에 적용하는 것 같습니다.
그런데 알파벡터와 베타벡터의 정의가 모호합니다.
알파벡터는 시그마에서 나오는 것 같습니다만
베타벡터는 어디에서 나온 것인지 궁금하고
알파를 베타로 바꾸는 과정에서 알파m과 베타 n의 매칭은 어찌 해야하는지 궁금합니다.
알파와 베타 모두 그냥 타입변수가 아닌가요.??
단지 인덱스가 같은것을 매칭하는것은 아닌것 같은데요
그리고 또 한가지는
M알고리즘에서 동일화 알고리즘을 사용하는데
동알화 알고리즘이 지난 숙제에 비해 달라진 것이 있습니까??
동일화 알고리즘의 리턴값은 S인데 이건 타입을 받아서 타입을 리턴하는 것으로 썼습니다.
그런데 M알고리즘에서
인용: | S1감마 + x: S1 베타1........ |
이런 식이 보이는데 S1에 베타1을 적용하면 원래대로라면 타입이 나옵니다.
그런데 이것이 추가되는 타입환경 감마는 다형타입 시스템에서
변수->타입틀 의 꼴인데요. S1 베타1 이 타입틀이 나와야하는것 아닌가요? |
|