可计算函数的逻辑

可计算函数的逻辑（LCF）是RobinMilner和合作者在1970年代初在斯坦福和爱丁堡开发的交互式自动定理检验器，基于DanaScott之前提出的可计算函数的逻辑的理论基础。LCF系统的工作引入了通用编程语言ML，允许用户编写定理验证战术，支持代数数据类型、参数化多态性、抽象数据类型和异常。

该系统中的定理是一种特殊的定理抽象数据类型的术语。ML的抽象数据类型的一般机制确保定理的推导只使用定理抽象类型的操作所给出的推理规则。用户可以编写任意复杂的ML程序来计算定理；定理的有效性并不取决于这种程序的复杂性，而是来自抽象数据类型实现的合理性和ML编译器的正确性。

LCF方法提供了类似于生成显式证明证书的系统的可信度，但不需要在内存中存储证明对象。Theorem数据类型可以很容易实现，根据系统的运行时配置，可以选择存储证明对象，所以它概括了基本的证明生成方法。使用通用编程语言开发定理的设计决定意味着，根据所写程序的复杂性，有可能使用相同的语言来写分步证明、决策程序或定理证明器。

可信的计算基础底层ML编译器的实现增加了可信的计算基础。关于CakeML的工作产生了一个正式验证的ML编译器，缓解了一些这些担忧。证明程序的效率和复杂性定理证明经常受益于决策程序和定理证明算法，其正确性已经被广泛地分析了。在LCF方法中实现这些程序的一个直接方法要求这些程序总是从系统的公理、公设和推理规则中推导出结果，而不是直接计算结果。一个潜在的更有效的方法是使用反思来证明一个在公式上操作的函数总是给出正确的结果。

在随后的实现中，剑桥LCF。后来的系统简化了逻辑，使用总函数而不是部分函数，导致了HOL、HOLLight和支持各种逻辑的Isabelle证明助手。截至2019年，Isabelle证明助手仍然包含一个LCF逻辑的实现，即Isabelle/LCF。