関数を表示=？不可能です

cs.stackexchange https://cs.stackexchange.com/questions/6879

質問

これは、スキームで教えられている1年目のコンピューターサイエンスコースの研究室です。 https://www.student.cs.uwaterloo.ca/~cs135/assns/a07/a07.pdf

ラボの終わりに、基本的に停止の問題を提示し、関数を導入することで解決することが不可能であることを示しています diagonal, 、次のように定義されています。

(define (diagonal x)
  (cond
     [(halting? x x) (eternity 1)]
     [else true]))

どこ eternity 次のように定義されている非終了プログラムです (define (eternity x) (eternity x)). 。あなたが餌を与えたときにどうなりますか diagonal 入力としての独自の定義...？

これはすべてかなり標準的なものです。それから、ラボは次のように述べています。

本当の挑戦のために、テキストの演習20.1.3の終わりに提起された質問に固定的に答えて、そのfunction =？ 2つの関数のコードを表す2つのリストを消費します。これは、教会が彼の証拠で考慮した状況です。

だからそれの要点はそれです function=? 2つの入力を取得します。それぞれがリストであり、関数の定義を表します。つまり、フォームのリストです (define (id args ...) body ...). 。両方の関数が構文的に有効であり、すべての入力（ランタイムエラーなし）で終了すると仮定できます。 function=? 同じ入力が与えられたときに、2つの関数が常に同じ結果を返す場合にのみ真実を返します。例えば、

(function=? '(define (foo x) (* 2 x)) 
            '(define (bar x) (+ x x))) ; should return #t

(function=? '(define (foo x) (+ x 1)) 
            '(define (bar x) (+ x 2))) ; should return #f

今、 function=? 書くことは明らかに不可能です - 挑戦は 証明 それは無理だ。私はこれについてしばらく考えましたが、私が思いつくことができる最良の解決策は次のとおりです。

(define (disprove-function=? x)
  ((lambda (snip)
     (let ((self (list 'define '(disprove-function=? x)
                       (list snip (list 'quote snip)))))
       (if (function=? self '(define (id x) x))
           (list x)
           x)))
   '(lambda (snip) 
      (let ((self (list 'define '(disprove-function=? x)
                        (list snip (list 'quote snip)))))
        (if (function=? self '(define (id x) x))
            (list x)
            x)))))

基本的に、 disprove-function=? 標準のクイニング手法を使用して、独自のソースコード（変数を生成します self）、そして尋ねます function=? ID関数に相当する場合。もしも function=? #Fは言います disprove-function=? 常にアイデンティティ関数のように動作します。矛盾！もしも function=? #Tは言います disprove-function=? 常にアイデンティティとは異なる動作をします。特に、それはのように振る舞います list 働き。矛盾！したがって、 function=? 存在できません。 QED。

私の質問は、この問題にアプローチするためのよりエレガントな方法はありますか？私の解決策は...長くて醜いようです。それほど素敵ではありません diagonal 停止問題が解決できないことを証明するための機能。

NB：ヒントではなく、答えをください！これは宿題の質問ですが、そうではありません 私の 宿題の質問：私はこの大学に行きません！さらに、あなたがラボからわかるように、この質問は Enhancements カテゴリとマークの価値がないので、たとえあなたが私を信じていなくても、私に答えを与えることにはまだ問題はありません。最後に、私はすでに 持ってる 解決策、私はかなり正しいと確信しています。私はただいるのではないかと思っていました より良い 解決。

役に立ちましたか？

解決

停止問題を使用すると、良い解決策のように思えます。関数があるとします red それは関数のコードを取得します（または λターム）（または無型関数）、1つのステップを削減します（または β-Redex）その中に、結果の関数のコードを返します。また、関数があると仮定します normal 用語がある場合はそれが言う 通常のフォーム.

チューリングマシンの言語では、 red 1つのステップの計算となります normal 私たちが最終的な状態にあるときに真実を返すでしょう。

$ n $ステップの計算をシミュレートし、計算の終了に達した場合、$ 1 $の代わりに43ドルを返します。

(define (run t n)
  (if (= n 0) 1
    (if (normal t) 43
      (run (red t) (n-1)))))

次に、用語の実行が終了するかどうかを判断できます。

(define (one x) 1)
(define (terminate t) (not (function=? (run t) one)))

それから、通常の対角線の引数を使用できます。

(define (loop x) (loop x))
(define (f x) (if (terminate (code-of-application x (quote x))) (loop 0) 1)
(f code-of-f)

もしも f オンに終了します code-of-f それから (terminate (code-of-application code-of-f (quote code-of-f)) 戻ります true その後 f ループします code-of-f. 。したがって、ループする必要があります。それで (terminate ...) 返す必要があります false と f で終了します code-of-f, 、矛盾。

技術：すべてを書くことができるほど表現力豊かな基本言語を定義する必要があります。その後、必要です red と normal 想像できるよりも厳しい場合があります。標準的なクインテクニックも必要です。 quote 用語のコードを考えると、用語のコードを表す用語を返します、 code-of-application a b 簡単で自明です。もちろん、あなたは内部的にすべてを書くために書く必要があります code-of-f.

ラムダカルクルスは、これをすべて書き留め、その正確性を証明するために驚くほどシンプルで表現力があります。そのため、教会はそれを解決するために使用しました ヒルバートの10番目の問題, 、しかし、言語固有のクイントリックを使用して、おそらくより簡単な方法で多くの言語でそれを行うことができます。

ライセンス： CC-BY-SA と 帰属
所属していません cs.stackexchange
scroll top