Warm tip: This article is reproduced from serverfault.com, please click

proof-用给定语言证明函数的不可表达性

(proof - Proving the inexpressibility of a function in a given language)

发布于 2020-12-13 21:16:07

我目前正在阅读John C. Mitchell的《编程语言基础》从本质上讲,练习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。

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

Questioner
Ben
Viewed
11
Ryan Culpepper 2020-12-14 19:43:18

没有解决方案,仅提示:

首先,我要指出的是,如果在语言穷个号码,然后幂定义为一个表达式。(你必须定义在无法表示真实结果(例如,环绕)的情况下应产生的结果。)请考虑原因。

提示:假设只有两个数字,0和1。你能写一个包含mn结果为的表达式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以某种方式存在错误...

你可以从Euclid证明存在无限多个素数的策略中找到一些启发。