Mechanizing Coinduction and Corecursion in Higher-Order Logic
Mechanizing Coinduction and Corecursion in Higher-Order Logic
复制标题
高阶逻辑中的机械化共归纳和共递归
DOI：
10.1093/logcom/7.2.175
复制
发表时间：
1997
期刊：
影响因子：
--
通讯作者：
Lawrence Charles Paulson
中科院分区：
文献类型：
--
作者：
Lawrence Charles Paulson
递归和共生放流的理论已在高阶逻辑（HOL）中发展，并使用isabelle机械化。至少flxedpoints表达归纳数据类型，例如严格列表；最大的flxedpoints表示共同传感数据类型，例如懒惰列表。良好的递归表达了归纳数据类型的递归功能。 Corecursion表达了产生共同数据类型元素的功能。该理论取决于传统的Inflite树的形式化。该理论旨在用于指定和验证。它支持有关广泛的可计算功能的推理，但它并未形式化其操作语义，并且也可以表达不可误的功能。该理论是使用Flnite和Inflite列表来说明的。 Corecursion表达在Inflite列表上的功能；有关此类功能的共同诱导原因。
A theory of recursive and corecursive deflnitions has been developed in higher-order logic (HOL) and mechanized using Isabelle. Least flxedpoints express inductive data types such as strict lists; greatest flxedpoints express coinductive data types, such as lazy lists. Wellfounded recursion expresses recursive functions over inductive data types; corecursion expresses functions that yield elements of coinductive data types. The theory rests on a traditional formalization of inflnite trees. The theory is intended for use in speciflcation and veriflcation. It supports reasoning about a wide range of computable functions, but it does not formalize their operational semantics and can express noncomputable functions also. The theory is illustrated using flnite and inflnite lists. Corecursion expresses functions over inflnite lists; coinduction reasons about such functions.