时间戳

首页 > 解决方案 > 证明给定语言中函数的不可表达性

programming-languages - 证明给定语言中函数的不可表达性

问题描述

我目前正在阅读 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 不能通过该语言中的表达式隐式定义。

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

标签： programming-languagesproofcomputability

解决方案

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

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

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

推荐阅读