CoLF Logic Programming as Infinitary Proof Exploration

TL;DR

The paper addresses the challenge of expressing infinitary proofs and objects within logic programming by developing computation-as-proof-construction over the first-order fragment $CoLF^{\omega}_1$. It introduces a channel-based, concurrent computation model where logic variables act as communication channels and combines static mode/uniqueness checking with compilation to the parallel language $Sax$ to avoid backtracking. Through examples with conatural numbers and streams, including $repeat$, $up$, $fib$, and $integrate$, the work demonstrates incremental, non-blocking proof construction and parallel evaluation of premises. The approach lays groundwork for extending to the full $CoLF^{\omega}$, promising a robust framework for infinitary proofs and their executable interpretations, with potential impact on proof systems, type theory, and concurrent logic programming.

Abstract

Logical Frameworks such as Automath [de Bruijn, 1968] or LF [Harper et al., 1993] were originally conceived as metalanguages for the specification of foundationally uncommitted deductive systems, yielding generic proof checkers. Their high level of abstraction was soon exploited to also express algorithms over deductive systems such as theorem provers, type-checkers, evaluators, compilers, proof transformers, etc. in the paradigm of computation-as-proof-construction. This has been realized in languages such as $λ$-Prolog [Miller et al., 1991] or Elf [Pfenning, 1991] based on backward chaining, and LolliMon [Lopez et al., 2005] or Celf [Schack-Nielsen and Schuermann, 2008], which integrated forward chaining. None of these early frameworks supported the direct expression of infinitary objects or proofs, which are available in the recently developed CoLF$^ω$ [Chen, 2023]. In this work-in-progress report, we sketch an approach to computation-as-proof-construction over the first-order fragment of CoLF$^ω$ (called CoLF$^ω_1$ ) that already includes infinitary objects and proofs. A key idea is the interpretation of logic variables as communication channels and computation as concurrent message-passing. This is realized in a concrete compiler from CoLF$^ω_1$ to Sax, a proof-theoretically inspired parallel programming language based on the proof-reduction in the semi-axiomatic sequent calculus [DeYoung et al., 2020].