paperbot · PL 论文追踪

全部论文 待读 收藏

P2 How much is in a square? Calculating functional programs with squares

方形中有多少?用方形计算函数式程序
JFP vol.352025匹配度 2/10 · 论文属于函数式编程的关系式演算与形式语义,侧重以交换方形进行程序计算与泛型理论,未涉及 LLM/Agent、静态分析、浮点程序分析或贝叶斯程序分析等画像核心交叉方向。引用 0 inbox
JOSE NUNO OLIVEIRA
crossref: 2026-09-10

AI 速览

一句话:提出以(半)交换方形为核心的关系式图形演算,用于计算函数式程序并给出 foldr/foldl 的泛型无归纳理论。

该文源于在关系基础上教授函数式编程的经验,主张采用一种图形化的表达与推理风格,其核心是(半)交换方形,作者在课堂中称之为“魔方”。魔方的边为二元关系,方形本身比较两条各含两条边的路径;魔方可组合并具有若干有用性质。文中给出跨逻辑、函数式编程、数据库建模和形式语义等领域的多个示例,并说明 free-theorem 方形尤为优雅且富有产出。借助少量 Galois 连接,作者给出 foldr 与 foldl 的泛型、无归纳理论,特别表明 foldl s = foldr (flip _s) 在比通常更弱的条件下成立。

问题
如何用直观、可组合的图形化关系推理来统一和简化函数式程序的计算与教学。
方法
以(半)交换方形为基本结构,将二元关系置于方形边上,通过方形比较两条路径;结合 free theorem 方形和 Galois 连接展开程序计算。
评估
通过逻辑、函数式编程、数据库建模、形式语义等跨领域示例说明该风格的有效性,并导出 foldr/foldl 的泛型无归纳理论及二者相等的新条件。
原文摘要(Abstract)

Abstract Experience in teaching functional programming (FP) on a relational basis has led the author to focus on a graphical style of expression and reasoning in which a geometric construct shines: the (semi) commutative square. In the classroom this is termed the “magic square” (MS), since virtually everything that we do in logic, FP, database modeling, formal semantics and so on fits in some MS geometry. The sides of each magic square are binary relations and the square itself is a comparison of two paths, each involving two sides. MSs compose and have a number of useful properties. Among several examples given in the paper ranging over different application domains, free-theorem MSs are shown to be particularly elegant and productive. Helped by a little bit of Galois connections, a generic, induction-free theory for ${\mathsf{foldr}}$ and $\mathsf{foldl}$ is given, showing in particular that ${\mathsf{foldl} \, {{s}}{}\mathrel{=}\mathsf{foldr}{({flip} \unicode{x005F}{s})}{}}$ holds under conditions milder than usually advocated.

链接与引用

DOI 原文 · PDF(开放获取) · DBLP

BibTeX
@article{Oliveira25,
  title = {How much is in a square? Calculating functional programs with squares},
  author = {JOSE NUNO OLIVEIRA},
  journal = {Journal of Functional Programming},
  volume = {35},
  year = {2025},
  doi = {10.1017/s0956796825000012}
}