我目前正在阅读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。
凭直觉,我愿意接受这一点。如果我们将幂运算视为重复乘法,则似乎我们“无法”用这种语言来表达。但是如何正式证明这一点呢?更广泛地说,你如何证明一种语言的表达不能用另一种语言表达?
没有解决方案,仅提示:
首先,我要指出的是,如果在语言穷个号码,然后幂是定义为一个表达式。(你必须定义在无法表示真实结果(例如,环绕)的情况下应产生的结果。)请考虑原因。
提示:假设只有两个数字,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
都以某种方式存在错误...
你可以从Euclid证明存在无限多个素数的策略中找到一些启发。