이 재귀 함수를 기반으로 측정 함수를 어떻게 결정합니까?

Question

함수는 ACL2에 정의되어 있으며 종료를 증명하는 데 도움이되는 측정 함수를 작성해야합니다. 이 함수의 정의입니다 :

(defunc f (x a) 
    :input-contract (and (integerp x) (listp a)) 
    :output-contract (integerp (f x a)) 
    (cond 
    ((endp a)     68) 
    ((equal (len a) x)  71) 
    ((equal (len a) (+ x 1)) 74) 
    ((< x (len a))   (f (+ x 1) (rest a))) 
    (t      (f (- x 1) (cons 1 a))))) 

그리고 솔루션 측정 기능입니다이 (속기) :

(m x a) = (if (equal (len a) (+ x 1)) 
       0 
       (abs (- (len a) x))) 

우리는 기반 포함된다 측정 기능의 다른 사례를 확인할 수 있었다 함수에서 두 개의 재귀 호출. 그러나 우리는 나머지 부분을 이해하지 못하고이 측정 기능을 파악하는 과정을 거쳤습니다. 참고로

, 측정 기능 :

1. 미터는 F의 파라미터 위에 네드 허용 함수 드 인터넷이고;
2. m은 f와 동일한 입력 계약을 갖습니다.
3. m에는 항상 자연수를 반환한다는 출력 계약이 있습니다. 재귀 호출시마다
4. 이 반환되며, 재귀 호출을 발생시키는 조건 하에서 해당 재귀 호출에 대한 인수에 적용된 m은 감소합니다 ( ).

이 측정 기능을 결정하는 과정은 무엇입니까?

Answer 1

측정 기능을 결정할 때 스스로에게 묻는 질문은 다음과 같습니다. 각 반복마다 다 소모 된 "잠재적 에너지"는 무엇이며 어느 시점에서 모두 사라지고 반복이 멈출 때까지 무엇입니까?

처음 보는 곳은 일반적으로 종료 조건입니다. 이 경우에는 세 가지가 있지만 마지막 두 가지가 가장 흥미 롭습니다. x과 (len a)의 차이가 너무 작 으면 반복을 중지한다고 말합니다.

그러면 잠재적 인 에너지가 (len a)과 x의 차이일까요? 그것이 합리적인지 여부를 확인하려면 재귀 적 사례를 확인하고 각 사례가 어느 정도 에너지를 소비하는지, 즉 차이를 줄이는지 확인해야합니다. 상황이 여기에 꽤 좋은 모양 미만 (len a) 우리는 그 다음 반복에 될 것 1 x을 증가시키고 그들 사이의 차이가 N, 그래서 경우 1 씩 (len a)을 감소입니다

• x 경우 N -2이 아닌 한, x = (len a)-1,이 아니면
• 그렇지 x(len a)보다 크고 그 차이가 N 후 다음 반복에있을 것 인 경우, 우리는 1 x 감소하고 다시 1만큼 (len a) 증가 N-2않는 X = (len a) + 1.이 두 하지 않는 조항의 성가신 세부 사항을 처리하기 때문에

는 거기에서 그것은 우리가 우리의 "낮은 에너지 상태"로 X = (len a) + 1을 선택해야합니다 있는지 매우 간단합니다.