Have a thing? Reasoning around recursion with dynamic typing in grounded arithmetic
Elliot Bobrow, Bryan Ford, Stefan Milenković
经典和直觉逻辑传统都不是与计算推理的目的完全一致的,因为逻辑传统通常都不能允许直接表达任意的一般递归函数而不不一致。 我们引入了基础算术或GA,这是形式推理的一个极简但强大的基础,允许直接表达任意递归的定义。 GA调整了传统的推理规则,使得表示非终止计算的术语无害地表示没有语义值(即“底部”),而不是导致逻辑悖论或不一致。 递归函数可以在GA中证明终止,主要是通过“动态类型”术语,或者等价地,象征性地反向执行它们通过GA的推理规则表示的计算。 一旦递归函数被证明终止,关于其结果的逻辑推理就会减少到熟悉的经典规则。 Isabelle/HOL中机械检查的一致性证明存在于GA的基本无量分片中。 量化器可以作为普通计算添加到此基础之上,因此其推理规则可接受,并且不会引入新的不一致风险。 虽然GA只是迈向手动或自动计算推理中日常使用的丰富类型接地演绎的第一步,但它表明,原则上可以将任意递归定义的表达自由纳入正式系统。
Neither the classical nor intuitionistic logic traditions are perfectly-aligned with the purpose of reasoning about computation, in that neither logical tradition can normally permit the direct expression of arbitrary general-recursive functions without inconsistency. We introduce grounded arithmetic or GA, a minimalistic but nonetheless powerful foundation for formal reasoning that allows the direct expression of arbitrary recursive definitions. GA adjusts the traditional inference rules such t...