显示功能=？是不可能的

Question

这是一年级计算机科学课程的实验室，该课程在方案中教授： 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=? 采用两个输入。每个都是一个列表，代表函数的定义，即它是表单的列表 (define (id args ...) body ...). 。我们可以假设两个函数在语法上都是有效的，并且将对所有输入（无运行时错误）终止。 function=? 当给出相同的输入时，且仅当两个函数始终返回相同的结果时，返回true。例如，

(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=? 如果它等于身份函数。如果 function=? #F说，然后 disprove-function=? 总是像身份功能一样行事。矛盾！如果 function=? ＃t，然后 disprove-function=? 始终将与身份不同；特别是，它的行为就像 list 功能。矛盾！因此， function=? 不存在。 QED。

我的问题是：是否有一种更优雅的方法来解决这个问题？我的解决方案似乎...漫长而丑陋。不像 diagonal 证明停止问题是无法解决的功能。

NB：请给我答案，而不是提示！即使这是一个家庭作业问题，也不是 我的 作业问题：我不去这所大学！此外，正如您可以从实验室中看到的那样，这个问题在 Enhancements 类别也不值得，所以即使您不相信我，也只有给我一个答案仍然没有问题。最后，我已经 有 我肯定是正确的解决方案；我只是想知道是否有 更好的 解决方案。

Answer 1

使用停止问题似乎是一个很好的解决方案。假设您有一个功能 red 这是函数的代码（或 λ任期）（或一个未型功能），减少一个步骤（或 β-雷克斯）并返回结果函数的代码。还假设您有一个功能 normal 那说如果该术语在 正常形式.

在图灵机语言中， red 将是一个步骤的计算 normal 当我们处于最终状态时，将返回真实。

让我们模拟$ n $ step的计算，如果我们达到计算结束，则返回$ 43 $而不是$ 1 $：

(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 这可能比人们想象的要难。您还需要标准Quine技术： quote 鉴于该术语的代码，它返回代表该术语代码的术语， code-of-application a b 简单且不言而喻，当然您需要在内部写所有内容才能写作 code-of-f.

Lambda-calculus令人惊讶地简单地表达了所有这些写下来并证明其正确性，这就是为什么教会用它来解决的原因 希尔伯特的第十个问题, ，但是人们可以使用特定于语言的Quine技巧，以更简单的方式来做很多语言。