2

関数は 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)))

関数内の 2 つの再帰呼び出しに基づいて、測定関数の else ケースが含まれると判断できました。しかし、その残りの部分と、このメジャー関数を理解するためのプロセスは理解できていません。

参考までに、メジャー関数:

  1. m は、f のパラメーターで定義された許容関数です。
  2. m は f と同じ入力契約を持っています。
  3. m には、常に自然数を返すことを示す出力コントラクトがあります。と
  4. 再帰呼び出しごとに、その再帰呼び出しの引数に適用される m は、再帰呼び出しにつながった条件下で減少します。

この測定関数を決定するに至ったプロセスは何ですか?

4

1 に答える 1

1

測定関数を決定する際に自問する質問は次のとおりです: ある時点ですべてがなくなり、反復が停止するポイントまで、各反復で使い果たされる「ポテンシャル エネルギー」は何ですか?

通常、最初に確認するのは終了条件です。xこの場合は 3 つありますが、最後の 2 つは最も興味深いものです:との差(len a)が小さすぎる場合は反復を停止すると言われています。

これにより、アイデアが得られます: 位置エネルギーが と の差である場合はどうなる(len a)でしょxうか? それが理にかなっているかどうかを確認するには、再帰的なケースをチェックして、それぞれがエネルギーを消費していること、つまり差が減少していることを確認する必要があります。物事はここでかなりよく見えます:

  • xより小さい場合は、1(len a)ずつ増やしxて 1 減らし(len a)ます。したがって、それらの差がnの場合、次の反復では、x = - 1でない限り、 n-2になります。(len a)
  • それ以外の場合xはより大きく、 1 ずつ(len a)減らしxて 1 ずつ増やし(len a)ます。ここでも、それらの差がnの場合、次の反復ではx = + 1でない限りn-2になります。(len a)

そこから、「低エネルギー状態」としてx = (len a)+ 1を選択する必要があることが非常に簡単にわかります。これは、これら 2 つのunless節の厄介な詳細を処理するためです。

于 2013-03-24T15:45:22.580 に答える