什么是可计算函数逻辑(LCF)？可计算函数、逻辑关联及LCF风格咨询

Logic for Computable Functions (LCF)是20世纪70年代初由Robin Milner及其合作者在斯坦福大学和爱丁堡大学开发的交互式自动定理证明器，基于Dana Scott此前提出的可计算函数逻辑理论基础构建。

1. 什么是可计算函数？ #

简单来说，可计算函数指的是存在明确的有限步算法可以算出结果的函数：你给它合法输入，就能按照无歧义的固定规则一步步计算，最终一定会得到确定的输出，不存在无限卡死、规则模糊无法执行的情况。
现在业界通用的可计算性定义和图灵机完全等价，只要是能通过图灵机实现的函数都属于可计算函数。日常接触的绝大多数函数都是可计算的，比如整数加法、字符串排序；而类似“给定任意一段程序，判断它会不会无限死循环”对应的函数就是不可计算的，至今不存在通用的有限步算法能实现这个功能。

2. 逻辑与可计算函数之间存在什么关联？ #

二者的核心关联是库里-霍华德同构（Curry-Howard correspondence），本质是双向映射关系：

• 逻辑系统里的命题对应可计算函数的类型
• 命题的合法证明对应对应类型的可计算函数/可执行程序
  具体到LCF的理论基础，Dana Scott提出的可计算函数逻辑就是把可计算函数的运行行为转化为逻辑命题描述，这样我们就能用严谨的逻辑推导，证明某个可计算函数/程序的运行结果完全符合预期，不会出现预期外的bug。反过来，逻辑推导的每一步规则都可以对应成可计算的操作，这也是定理证明器能自动校验证明是否合法的核心依据。

3. 什么是LCF-style？ #

LCF-style是现在包括Isabelle、Coq、HOL系列在内的主流交互式定理证明器普遍采用的设计范式，核心设计思路可以归纳为三点：

• 仅极小的核心推理内核被视为可信组件，所有证明的每一步最终都要经过内核的基础推理规则校验，只要内核没有逻辑bug，最终得到的定理就一定是正确的，不需要信任上层的各类自动化证明策略代码
• 定理本身被定义为抽象数据类型，只有内核有权限生成合法的定理类型值，上层逻辑无法绕过内核构造非法的假定理
• 支持用户自由自定义证明策略、自动化处理流程，不用担心自定义代码会破坏证明的正确性，所有自定义策略生成的证明步骤最终还是要经过内核校验后才会被承认。

内容的提问来源于stack exchange，提问作者flyingsheep