1

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

<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 不能通过该语言中的表达式隐式定义。

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

4

2 回答 2

2

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

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

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

于 2020-12-14T12:56:18.507 回答
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是错误的......

你可能会从欧几里得证明有无限多个素数的策略中找到一些灵感。

于 2020-12-14T11:43:18.773 回答