Vector Graphics through Category Theory

doi:10.1007/978-3-032-07021-0_24

Vector Graphics through Category Theory

2026-01-01

0

PRE

AI

D

Davi Sales Barreira *

DOI：10.1007/978-3-032-07021-0_24

原文链接

原文求助

摘要

En 中文

本文介绍了一种在范畴论（CT）框架下形式化矢量图形绘制的新方法。采用范畴编程范式，将CT抽象解释为函数式编程（FP）中的设计模式，从而连接理论形式化与实际实现。基于Yorgey的工作，我们将图形表示为图形原语的列表，作为矢量图形的正则形式。通过图形变换（如平移、旋转、缩放、颜色改变）和列表连接操作对图形进行操作，这些操作被建模为一个自函子F。这使我们能够构建一个与Free F同构的自由单子T，以实现将操作积累到表达式树中的惰性方式。我们通过分片范畴将图形标记形式化为对图形的抽象，并将矢量图形定义为自由单子T上的标记值。最后，我们引入图形表达式，利用F代数和F余代数系统性地构建复杂图形。一个基于依赖类型编程语言的Lean原型实现展示了我们的理论在实践中的应用，说明了范畴编程如何弥合数学抽象与实际编程之间的差距。Julia实现将在其他地方呈现。

Keyword:

Vector Graphics

Category Theory

Diagrams

Functional Programming

Lean

Vector Graphics through Category Theory

摘要

期刊

机构

引用论文