Iteration Theories and Data Type Specifications

在与Elgot和Wright的联合工作中，PI使用了 流程图控制结构公理化中的迭代理论 算法 迭代理论似乎也提供了一个 公理化 对于循环抽象数据类型的函子描述， 最近由Smyth，Lehmann，Plotkin，Arbib Manes， 等人 PI现在正在调查迭代的适用性 描述抽象数据类型的理论。 它被 确定是否可以使用相同的等式公理来描述 程序的控制结构和数据结构 类型、操作和程序操作的域。 也 正在进行的是算法的发展， 关于数据类型描述的等价性的问题：给定 两个描述（作为某些内函子的不动点），它们 描述“同一件事” 这个问题类似于这个问题： 给定两个流程图方案，它们有保存行为吗？ 验证了迭代理论与 正如PI所期望的那样，数据类型将表明这两个问题是 一模一样 这项拟议中的研究预计将导致更好的理解 数据类型。 PI在相关研究方面有着良好的记录 成就。

In joint work with Elgot and Wright, the PI used the notion of iteration theories in axiomatizing the control structure of flowchart algorithms. Iteration theories also appear to provide an axiomatization for the functorial description of circular abstract data types as described most recently by Smyth, Lehmann, Plotkin, Arbib & Manes, and others. The PI is now investigating the suitability of iteration theories for the description of abstract data types. It is being determined whether the same equational axioms can be used to describe both the control structure of programs and the structure of the data types, operations and domains on which the programs operate. Also in progress is the development of algorithms for the solution of problems concerning the equivalence of data type descriptions: Given two descriptions (as fixed points of certain endofunctors), do they describe the "same thing"? The question is analogous to the question: Given two flowchart schemes, do they have the save behavior? Verification that the connection between iteration theories and data types is as the PI expects will show that these two questions are identical. The proposed research is expected to lead to an improved understanding of data types. The PI has a fine record of related research accomplishments.