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