首页/论文/0909.3596

arXiv 0909.35962009-09-19cs.LOmath.LO

用初始代数构造数据对象

Specifying Data Objects with Initial Algebras

Chris Preston

备注：: 120 pages

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

摘要英文摘要相关论文

摘要：

这项研究提出了一个系统的方法来指定数据对象的帮助下，初始代数。主要目的是描述现代函数式程序设计语言（如Haskell和ML）中的设置，尽管它也可以应用于更一般的情况。

英文摘要：

This study presents a systematic approach to specifying data objects with the help of initial algebras. The primary aim is to describe the set-up to be found in modern functional programming languages such as Haskell and ML, although it can also be applied to more general situations.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

摘要英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

可呈现的签名与初始语义

Presentable signatures and initial semantics

本文提出可呈现签名框架，用于指定数据类型和编程语言语法，通过初始语义生成语法，涵盖变量绑定并支持组合构造，且经计算机验证。

2021-05-25cs.LOcs.PL

解除限制的初始代数——一种在Agda中形式化的新型初始代数构造

Initial Algebras Unchained -- A Novel Initial Algebra Construction Formalized in Agda

该研究提出一种不依赖序数索引链的新型初始代数构造方法，通过构造所有有限递归余代数的余极限得到初始代数，证明为构造性且已在Agda中完全形式化。

2024-05-21cs.LO

初始代数上的Fibular初始代数-最终余代数重合：颠倒验证见证

Fibrational Initial Algebra-Final Coalgebra Coincidence over Initial Algebras: Turning Verification Witnesses Upside Down

The Graduate University for Advanced Studies (SOKENDAI)（综合研究大学院大学）；National Institute of Informatics（国立情报学研究所）

初始代数（IA）和最终余代数（FC）之间的重合是理论计算机科学中各种重要结果的基础。在本文中，我们确定了IA-FC重合的一般纤维条件，即在纤维上的基范畴中的初始代数。将纤维中的（co）代数识别为（co）归纳谓词，我们的纤维IA-FC重合允许使用共归纳证人（如不变量）来验证归纳性质（如活性）。我们的一般纤维化理论的特点链colimits的稳定性的技术条件，我们扩展的框架存在的一元效应，也限制到纤维化的完整格值谓词。我们的分类理论的实际好处是例证了新的“颠倒”证人概念的三个验证问题：概率活性，接受和模型检查自下而上的树自动机。

2021-08-24cs.CLcs.LO

一个不需迭代的初始代数定理

An Initial Algebra Theorem Without Iteration

Trnková等人的初始代数定理国家，在温和的假设下，一个endofunctor有一个初始代数提供了它有一个预固定点。证明关键取决于transmitting迭代函子，事实上表明，等价地，（超限）初始代数链停止。给出了初始代数定理的构造性证明，避免了函子的超限迭代。对于函子的给定预不动点$A$，利用Pataraia定理得到了单调函数在由$A$的所有子代数构成的偏序上的最小不动点.由于递归余代数的性质，这个最小不动点产生一个初始代数。我们获得了新的结果，不动点和初始代数的类别丰富的有向完全偏序，再次没有迭代。使用超限迭代，我们等价地获得收敛的初始代数链作为一个等价条件，整体上产生一个简化版本的原始证明。

2022-02-14cs.LOmath.CT

将代数作为抽象数据类型处理

Process Algebra as Abstract Data Types

本文以抽象数据类型的形式介绍了进程代数的代数语义。为此，我们开发了一种特殊类型的代数，种子代数，它精确地描述了标记转移系统中进程的行为。我们已经证明了两个进程的互模拟与它们相应的种子代数的同构的可能性。我们指出，传统的代数同构概念在这里并不适用，因为两个种子代数的元素之间甚至不存在一一对应。这种一一对应的缺乏来自于过程转换的非确定性选择。我们引入了一种隐藏操作的技术来屏蔽种子代数元素中不需要的细节，这些细节只反映了进程转换的非确定性或其他隐式控制机制。种子代数的元素被认为是不可区分的，如果他们表现出相同的行为后，这些不必要的细节被掩盖。每一类不可区分的元素称为非隐藏闭包。我们证明了两个过程的互模拟等价于表示这两个过程的两个种子代数的非隐闭包的同构。我们称这种同构为深层同构。通过对同一个签名指定不同的公理系统，得到了不同的种子代数模型。每个模型对应于不同类型的互模拟。通过证明这些模型之间的关系，我们还建立了10个不同的互模拟之间的关系，形成一个无环有向图。

2010-01-07cs.LOcs.PL

作为同伦初始代数的高阶归纳型

Higher Inductive Types as Homotopy-Initial Algebras

同伦类型论是基于马丁-洛夫构造性类型论和抽象同伦理论之间令人惊讶的和优雅的对应关系的一个新的数学领域。我们在这些学科之间有着强大的相互作用--我们可以使用几何直观来表述类型论中的新概念，相反，我们可以使用类型论的机器来验证并经常简化现有的数学证明。这个新系统中的一个关键成分是更高的归纳类型，它允许我们表示诸如球体、环面、推出物和平行物之类的对象。我们研究了一种高阶归纳类型的变体，它的计算行为取决于一个高阶路径，我们证明了在这种情况下，高阶归纳类型的特征在于它是一个同伦初始代数的泛性质.

2014-02-04cs.LOmath.CTmath.LO

更多相关论文收起更多论文

Beyond初始代数与最终余代数

Beyond Initial Algebras and Final Coalgebras

本文给出了一个函子的不动点的构造，这些函子可以不是初始代数或最终余代数。对于一个内函子F，这个不动点结构可以表示为F-余代数和F-代数之间的一对伴随函子。我们证明了这些广义不动点的极限余限重合定理的一个版本。

2023-03-03cs.LOmath.CT

用膨胀迭代法构造初始代数

Constructing Initial Algebras Using Inflationary Iteration

经典集合论中的Adámek的一个老定理通过序数上的超限迭代构造了充分共连续的内函子的初始代数。我们证明了一个新的版本，工程建设性的逻辑，使用“通货膨胀”迭代的大小概念，抽象的极限序数只是他们的传递性，定向和良好的基础属性。借用泰勒的建设性的序数处理，我们表明，存在的大小与上界的任何给定的签名的指数。由此可以得出结论，只要人们承认由于Streicher、Moerdijk、van den Berg和Palmgren而产生的弱选择形式（WISC），就有丰富的一类内函子可以应用新定理，并且已知它在许多种拓扑的内部构造性逻辑中成立。

2022-11-03cs.LOmath.CTmath.LO

循环共享树结构的初始代数语义

Initial Algebra Semantics for Cyclic Sharing Tree Structures

术语是树结构的简明表示。由于它们可以通过归纳类型自然地定义，因此它们在函数式编程和机械化推理中提供了数据结构，并具有有用的原则，如结构归纳和结构递归。然而，对于图或“树状”结构--包含循环和共享的树--仍然不清楚存在什么样的归纳结构，以及我们如何忠实地分配它们的术语表示。在本文中，我们提出了一个简单的术语语法循环共享结构，承认结构归纳和递归原则。我们表明，得到的语法是直接可用的函数式语言Haskell和证明助手Agda，以及普通的数据结构，如列表和树。为了实现这一目标，我们使用范畴的方法来初始代数语义的预层类别。这种方法遵循Fiore，Plotkin和Turi的变量绑定抽象语法模型。

2010-09-03cs.LO

可达性条件下的初始代数对应

Initial Algebra Correspondence under Reachability Conditions

本文提出范畴论统一框架，通过伴随函子导出抽象可达性条件，证明迁移系统中两种不动点语义及初始代数的一致性，并以MCs、自动机等为例验证通用性，还研究了马尔可夫决策过程下的规范构造。

2025-09-05cs.LO

Cedille中高阶抽象代数的弱初始代数

A Weakly Initial Algebra for Higher-Order Abstract Syntax in Cedille

Cedille是一个相对较新的工具，基于Curry风格的纯类型论，没有原始的数据类型系统。使用新技术的基础上依赖的交叉类型，归纳数据集及其归纳原则。这种方法的一个好处是它允许探索新的或高级形式的归纳数据类型。本文报告的工作进展中的一个这样的形式，即高阶抽象语法（HOAS）。我们在纯类型论的背景下考虑HOAS的性质，与传统的λ演算的环境模型的概念进行比较。我们看到了一种替代方案，基于我们所称的Kripke函数空间，我们可以在Cedille中推导出弱初始代数。使用编码给出了几个例子。

2019-10-24cs.LOcs.PL

代数余完备性与有限函子

Algebraic cocompleteness and finitary functors

提出了一些代数完备和共完备的范畴，即，每个内函子都有一个初始代数和一个终结余代数。对于所有有限（更一般地，所有预连续）集函子的初始代数和终端余代数进行一个规范偏序与相同的理想CPO-完成。而且它们都带有一个具有相同Cauchy完备化的正则超度量。

2021-05-05cs.LOmath.CT

良点余代数

Well-Pointed Coalgebras

对于保交簇的闭函子，给出了终余代数与初代数的新刻画：终余代数由所有良点余代数组成。这些是没有真子对象和真商的点余代数。初始代数由所有在Osius和Taylor意义下良基的良点余代数组成。而初始代数恰好是最终良基余代数。最后，初始迭代代数由所有有限良点余代数组成。许多例子进行了讨论，例如自动机，图形和标记的过渡系统。

2013-08-13cs.LOmath.CT