是否可以枚举计算机程序？

Question

假设您必须编写一个程序来测试所有程序以搜索完成特定任务的程序.例如,考虑这个JavaScript函数:

function find_truth(){
    for(n=0;;++n){
        try {
            var fn = Function(string(n));
            if (fn() == 42)
                return fn;
        } catch() {
            continue;
        }
    }
}

只要string(n)返回第n个字符串("a","b","c",......"aa","ab"......),该程序最终将输出一个求值的函数42.此方法的问题在于它枚举的字符串可能是也可能不是有效的程序.我的问题是:是否可以自己枚举程序？怎么样？

Answer 1

是的,有可能这样做.几个月前,我做了一个小实验项目,做了类似的事情,考虑到它正在做的事情,它运作得相当好.你给它一个类型和一些测试来传递,它搜索一个合适的函数来传递测试.我从来没有投入使其成熟,但你可以看到它实际上最终生成了在示例的情况下通过测试的函数.要求这种类型是这种搜索实用性的重要组成部分 - 它大大减少了需要尝试的程序数量.

在断言关于什么是不可能的事情之前,牢牢掌握这个理论是非常重要的 - 有许多人会跳到停止问题并告诉你这是不可能的,当真相更加微妙时比起那个来说.

• 您可以轻松生成给定语言的所有语法上有效的程序.天真地,您可以生成所有字符串并过滤掉解析/类型检查的字符串; 但还有更好的方法.
• 如果语言不完整 - 例如简单类型的lambda演算,或者甚至像Agda这样非常强大的东西,你可以枚举生成42的所有程序,并且给定任何程序你可以决定"这生成42"或"这样做不生成42".(我在实验项目中使用的语言在本课程中).这里的张力是,在任何这样的语言中,都会有一些你无法编写的可计算函数.
• 即使语言完成,您仍然可以枚举最终生成42的所有程序(通过并行运行它们来完成此操作,并在完成时报告成功).

你不能用图灵完整的语言来决定一个程序绝对不会产生42 - 它可以永远地运行,并且你无法判断它是否会最终成功直到它完成.有一些程序,你可以告诉会死循环,虽然,只是不是所有的人.因此,如果你有一个程序表,你可能希望你的枚举器程序在非图灵齐全的语言中是这样的:

Program |  P1  |  P2  |  P3  |  P4  |  P5  |  P6  |  P7  | ...
42?     | No   | No   | No   | Yes  | No   | No   | No   | ...

而在图灵完整语言中,您的输出(在给定时间)将如下所示:

Program |  P1  |  P2  |  P3  |  P4  |  P5  |  P6    |  P7  | ...
42?     | No   | No   | Loop | Yes  | No   | Dunno  | No   | ...

后来Dunno可能变成了Yes或No,或者它可能会永远留下dunno - 你只是不知道.

这一切都是非常理论化的,实际上用图灵完整语言生成程序来搜索那些做某件事的程序非常困难而且需要很长时间.当然你不想一个接一个地做,因为空间太大了; 您可能想要使用遗传搜索算法或其他东西.

理论中另一个微妙的观点:谈论"生成42"的程序缺少一些重要的细节.通常当我们谈论生成程序时,我们希望它生成某个函数,而不仅仅是输出特定的函数.这就是你想要做的事情变得更加不可能的时候.如果你有无限的可能输入空间 - 比如输入一个数字,那么

• 您通常无法判断程序是否计算给定的函数.您无法手动检查每个输入,因为无穷大太多而无法检查.你不能搜索你的函数做正确的事情的证据,因为对于任何可计算函数f,对于任何公理系统A,有计算f的程序使得A没有证明它们计算f.
• 你无法判断程序是否会为每个可能的输入提供任何答案.它可能适用于其中的前400,000,000个,但在400,000,001个上无限循环.
• 同样,您无法判断两个程序是否计算相同的功能(即相同的输入 - >相同的输出).

你有它,每日剂量的可判定性理论现象学.

如果您有兴趣真正做到这一点,请研究遗传算法,并对您尝试的功能和/或使用可判定的(非图灵完备)语言进行超时.