SICP의 통일 알고리즘에서 겉보기에 불필요한 경우

Question

SICP에 설명 된 통일 알고리즘을 이해하려고합니다. 여기

특히, "확장 -IF- 입술"절차에는 오른손 "표현"이 이미 무언가에 묶인 변수인지 확인하는 점검 (Asterix "*")이 있습니다. 현재 프레임 :

(define (extend-if-possible var val frame)
  (let ((binding (binding-in-frame var frame)))
    (cond (binding
       (unify-match
        (binding-value binding) val frame))
      ((var? val)                      ; *** why do we need this?
       (let ((binding (binding-in-frame val frame)))
         (if binding
             (unify-match
              var (binding-value binding) frame)
             (extend var val frame))))
      ((depends-on? val var frame)
       'failed)
      (else (extend var val frame)))))

관련 해설은 다음과 같습니다.

"첫 번째 경우, 우리가 일치하려는 변수가 제한되지 않지만, 우리와 일치시키려는 값은 그 자체가 (다른) 변수입니다. 값이 바인딩되었는지 확인해야합니다. 그렇다면 그 가치에 맞게. 경기의 양 당사자가 결점이없는 경우, 우리는 다른 사람에게 구속 될 수 있습니다. "

그러나 이것이 실제로 필요한 경우를 생각할 수 없습니다.

무슨 말을하는지, i 생각한다, 현재 다음 프레임 바인딩이있는 곳입니다.

{?y = 4}

그런 다음? z에서? y에서 "expendifpossible"을 "extendifpossible"하도록 요청받습니다.

"*"확인 참석, "? z"를 "? y"로 확장하라는 요청을 받으면 "? y"는 이미 4로 묶인 다음 "4"로 "? z"를 재귀 적으로 통일하려고합니다. "? z = 4"로 프레임을 확장 한 결과.

점검이 없으면 "? z =? y"만으로 프레임을 확장하게됩니다. 그러나 두 경우 모두 Z가 아직 다른 것에 묶여 있지 않은 한 문제를 보지 못합니다.

if? z 가졌다 이미 다른 것에 묶여 있으면 코드가 "*"라고 표시된 부분에 도달하지 못합니다 (우리는 이미 Z가 이미 일치 한 것과 통일로 되돌아 갔을 것입니다).

그것을 생각한 후, 나는 "가장 간단한"MGU (가장 일반적인 통합제)를 생성하기위한 일종의 주장이있을 수 있음을 깨달았습니다. 예를 들어 다른 변수를 언급하는 최소 수의 변수가있는 MGU를 원할 수 있습니다. 즉, 대체 {? x = 4,? ? y = 4} ...하지만이 알고리즘이 어떤 경우 에도이 동작을 보장 할 것이라고 생각하지 않습니다. "(? x 4)" "(? y? y)"그러면 당신은 그렇게 할 것입니다. 여전히 {? x =? y,? y = 4}로 끝납니다. 그리고 행동을 보장 할 수 없다면 왜 추가 복잡성이 있습니까?

여기서 내 추론이 모두 맞습니까? 그렇지 않은 경우, "*"점검이 옳은 mgu?

Answer 1

그건 좋은 질문이야!

그 이유는 당신이 다음과 같은 원형 바인딩으로 끝나고 싶지 않기 때문입니다 { ?x = ?y, ?y = ?x }. 특히 통일 (?x ?y) ~와 함께 (?y ?x) 수표를 생략하면 위의 원형 프레임을 줄 것입니다. 점검을 사용하면 예상대로 프레임 {? x =? y}를 얻습니다.

프레임의 원형 바인딩은 프레임을 사용하여 대체를 수행하는 기능을 유발할 수 있기 때문에 나쁘다. instantiate, 무한 루프로 실행됩니다.

Answer 2

그것 없이는 당신은 얻지 못할 것입니다 가장 일반 통일. x와 y를 통일하는 작업이 여전히 있습니다.