证明函数在给定语言中的不可表达性

Question

我目前正在阅读 John C. Mitchell 的编程语言基础。练习 2.2.3 本质上要求 reader 证明（自然数）指数函数不能通过小语言的表达式隐式定义。该语言由自然数和所述数字的加法（以及布尔值、自然数相等谓词和三元条件）组成。没有循环、递归结构或定点组合器。这是准确的语法：

<bool_exp> ::= <bool_var> | true | false | Eq? <nat_exp> <nat_exp> |
               if <bool_exp> then <bool_exp> else <bool_exp>
<nat_exp>  ::= <nat_var> | 0 | 1 | 2 | … | <nat_exp> + <nat_exp> |
               if <bool_exp> then <nat_exp> else <nat_exp>

同样，目的是表明求幂函数 n^m 不能通过这种语言的表达式隐式定义。

直觉上，我愿意接受这一点。如果我们将求幂视为重复乘法，似乎我们“无法”用这种语言表达它。但是如何正式地证明呢？更广泛地说，你如何证明一种语言的表达不能用另一种语言表达？

Answer 1

没有解决方案，只有提示：

首先，让我指出，如果语言中有有限多个数字，则求幂是可定义为表达式。（您必须定义当真实结果无法表示时它应该产生什么，例如环绕。）想想为什么。

提示：假设只有两个数字，0 和 1。你能写出包含 m 和 n 且结果为 n^m 的表达式吗？如果有三个数字：0、1 和 2 会怎样？如果有四个呢？等等...

为什么这些解决方案都不起作用？让我们索引它们并调用 {0,1} partial_solution_1 的解决方案、{0,1,2} partial_solution_2 的解决方案，依此类推。为什么 partial_solution_n 不是所有自然数集合的解？

也许你可以用一些度量 f : Expression -> Nat 以某种方式概括这一点，这样每个 expr 和 f(expr) < n 的表达式都是 错误的 不知何故......

你可能会从欧几里德证明素数无穷多的策略中得到一些启发。

Answer 2

这里有一个简单的思考方式：表达式具有固定的有限大小，它可以执行的唯一算术运算来生成不是以文字形式编写或作为变量值提供的数字是加法。所以它可能产生的最大数受加法次数加1乘以表达式中涉及的最大数的限制。

因此，给定一个提议的表达式，设 k 为其中的加法数，设 c 为最大文字（如果存在 none，则为 1）并选择 m 和 n，使得 n^m > (k+1)*max(m,n,c)。那么该输入的表达式结果不可能是正确的。

请注意，此证明依赖于允许任意大数的语言，如其他答案中所述。

证明函数在给定语言中的不可表达性

Proving the inexpressibility of a function in a given language

programming-languages

proof

computability