pith. machine review for the scientific record. sign in

arxiv: 2604.26161 · v1 · submitted 2026-04-28 · 💻 cs.PL

Recognition: unknown

Finite Functional Programming

Michael Arntzenius , Max Willsey
Authors on Pith no claims yet

Pith reviewed 2026-05-07 13:37 UTC · model grok-4.3

classification 💻 cs.PL
keywords functional programminglogic programmingfinite supporttype systemsDataloggraded effectsrelevance typesunification
0
0 comments X

The pith

Treating predicates as functions with finite support unifies functional and logic programming.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper establishes that logic programming constructs can be absorbed into functional programming by reinterpreting predicates as functions whose output is nonzero only on a finite set of inputs. This finite support property lets the functions be stored and manipulated as ordinary data tables instead of opaque code. Generalizing the output domain to pointed sets extends the same representation to aggregation and weighted logics without separate mechanisms. A type system using graded effects for grounding and relevance types for pointed sets enforces the finite-support invariant statically. If this holds, a single language can express both paradigms through ordinary higher-order functions and data.

Core claim

By equipping every function with its support—the finite set of inputs on which its output is nonzero—predicates become representable as input-output tables. Datalog is recovered exactly as the language of finitely supported boolean functions. Extending the codomain from booleans to arbitrary pointed sets uniformly accounts for aggregation and weighted logic programming. The resulting combination, called finite functional programming, interleaves finitely supported functions as data with ordinary higher-order functions as code, all checked by a type system that uses graded effects to enforce variable grounding and relevance types to model pointed sets.

What carries the argument

Finitely supported functions, where support is the finite set of inputs yielding nonzero output, allowing table representation, combined with higher-order code under a graded-effect type system.

If this is right

  • Datalog programs become ordinary expressions built from boolean functions whose support is finite and statically checkable.
  • Aggregation and weighted rules are obtained simply by changing the codomain to a pointed set while retaining the same table representation.
  • Variable grounding and relevance are enforced uniformly by graded effects and relevance types rather than by separate logic-programming machinery.
  • Functions can be freely mixed with higher-order code because finite support is a property of the data representation, not a separate language construct.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Compilers could translate logic queries directly into table-lookup operations, potentially improving performance for finite domains.
  • The approach suggests that hybrid languages could avoid duplicating syntax for declarative and procedural styles.
  • Similar finite-support restrictions might be applied to probabilistic or differentiable programming to keep representations tractable.

Load-bearing premise

Representing predicates as finitely supported functions (and generalizing their codomains to pointed sets) preserves the full semantics and expressiveness of logic programming without hidden limitations.

What would settle it

Existence of a standard logic-programming feature, such as stratified negation or certain forms of recursion, that cannot be expressed using any finitely supported function or enforced by the graded-effect and relevance-type system.

Figures

Figures reproduced from arXiv: 2604.26161 by Max Willsey, Michael Arntzenius.

Figure 1
Figure 1. Figure 1: Pointed sets I have known and loved types 𝐴, 𝐵 ::= 𝑃 | 𝐴 → 𝐵 | 𝐴 × 𝐵 | 1 | ... pointed types 𝑃, 𝑄 ::= 𝑃 & 𝑄 | 𝑃 ⊗ 𝑄 | 𝑃 ⊸ 𝑄 | 𝐴 ⇒ 𝑄 | maybe 𝐴 | N0 expressions 𝑒 ::= 𝑡 | 𝑥 | 𝜆𝑥. 𝑒 | 𝑒1 𝑒2 | (𝑒1, 𝑒2) | 𝜋𝑖 𝑒 | () case 𝑒1 of just 𝑥  𝑒2; none  𝑒3 | ... pointed terms 𝑡, 𝑢 ::= nil | 𝑥 | 𝜆𝑥. 𝑡 | 𝑡 𝑢 | 𝑡 𝑥 | 𝑡 𝑒 | ⟨𝑡, 𝑢⟩ | 𝜋𝑖 𝑡 (𝑡, 𝑢) | let (𝑥, 𝑦) = 𝑡 in 𝑢 | just 𝑒 | let just 𝑥 = 𝑡 in 𝑢 view at source ↗
Figure 2
Figure 2. Figure 2: Syntax of 𝜆FS The type of cross captures something important: curried functions preserve nil in all arguments separately, and since nil𝐴⇒bool = 𝜆_.false is the empty relation, we know from its type alone that the cross product of an empty set with any other relation is empty. Inner joins in general have this property because they use conjunction. For instance, intersection: intersect : (𝐴 ⇒ bool) ⊸ (𝐴 ⇒ 𝑏𝑜… view at source ↗
Figure 3
Figure 3. Figure 3: Syntax sugar and primitive functions in 𝜆FS filmCount : person ⇒ N0 filmCount actor = sum (𝜆film. 1 when stars film actor) In general, for any commutative monoid of the form (𝑃, ⊕, nil𝑃), since nil⊕nil = nil we have ⊕ : 𝑃 & 𝑃 ⊸ 𝑃. This extends to an aggregation É 𝑃 : (𝐴 ⇒ 𝑃) ⊸ 𝑃 that takes a finite map 𝑓 : 𝐴 ⇒ 𝑃 to the monoid sum É 𝑥∈supp 𝑓 𝑓 (𝑥). For instance, the aggregation of the monoid (bool, or, fals… view at source ↗
Figure 4
Figure 4. Figure 4: 𝜆FS typing rules view at source ↗
Figure 5
Figure 5. Figure 5: Semantics of types and contexts in 𝜆FS semantics of Γ ⊢ 𝑒 : 𝐴 ⟦𝑡⟧ 𝛾 = ⟦𝑡⟧ 𝛾 () () ⟦𝑥⟧ 𝛾 = 𝜋𝑥𝛾 ⟦()⟧ 𝛾 = () ⟦𝜆𝑥. 𝑒⟧ 𝛾 = 𝜆𝑥. ⟦𝑒⟧ (𝛾, 𝑥) ⟦𝑒1 𝑒2⟧ 𝛾 = ⟦𝑒1⟧ 𝛾 (⟦𝑒2⟧ 𝛾) ⟦(𝑒1, 𝑒2)⟧ 𝛾 = (⟦𝑒1⟧ 𝛾, ⟦𝑒2⟧ 𝛾) ⟦𝜋𝑖 𝑒⟧ 𝛾 = 𝜋𝑖(⟦𝑒⟧ 𝛾) ⟦case 𝑒1 of just 𝑥  𝑒2; none  𝑒3⟧ = ( ⟦𝑒2⟧ (𝛾, 𝑥) if ⟦𝑒1⟧ 𝛾 = just 𝑥 ⟦𝑒3⟧ 𝛾 otherwise semantics of Γ / Δ / Ω ⊢ 𝑡 : 𝑃 ⟦Γ / · / · ⊢ 𝑒 : 𝑃⟧ 𝛾 𝛿 = {() ↦→ ⟦𝑒⟧ 𝛾 : 𝛿 ≠ nil} ⟦Γ / Δ / Ω ⊢ nil : 𝑃⟧ 𝛾 𝛿 … view at source ↗
Figure 6
Figure 6. Figure 6: Semantics of expressions and terms in 𝜆FS view at source ↗
read the original abstract

We unify functional and logic programming by treating predicatesas functions equipped with their support: the set of inputs whose output is nonzero. Datalog, for instance, is a language of finitely supported boolean functions. Finite support allows representing functions as input-output tables. Generalizing from boolean functions to other pointed sets neatly handles aggregation and weighted logic programming. We refer to the combination of finitely supported functions, represented as data, with higher order functions, represented as code, as finite functional programming. We give a simple type system to check finite support, using graded effects to check variable grounding and relevance types to model pointed sets.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 1 minor

Summary. The paper proposes unifying functional and logic programming by modeling predicates as functions equipped with finite support—the set of inputs yielding nonzero outputs. Datalog is presented as the special case of finitely supported boolean functions, which can be represented as input-output tables. The approach generalizes to other pointed sets to handle aggregation and weighted logic programming. The combination of finitely supported functions (as data) with higher-order functions (as code) is termed finite functional programming. A type system is sketched that uses graded effects to enforce variable grounding and relevance types to model pointed sets and the distinguished zero element.

Significance. If the type system can be shown to be sound and to recover the full expressiveness of logic programming without hidden restrictions, the work would provide a uniform functional foundation for hybrid paradigms. Representing predicates directly as tables via finite support, combined with graded effects and relevance, could simplify implementations of Datalog-style systems and weighted logics inside functional languages, while preserving higher-order programming.

major comments (2)
  1. [Abstract] Abstract: the unification and type system are asserted without any formal semantics, typing rules, derivations, or even small examples of how graded effects check grounding or how relevance types interact with higher-order functions; the central claim therefore cannot be verified from the provided text.
  2. [Abstract] Abstract: the weakest assumption—that finitely supported functions over pointed sets preserve the full semantics and expressiveness of logic programming without additional mechanisms—is stated but not demonstrated; no argument is given showing that the representation as input-output tables plus the proposed type system recovers standard Datalog operations or aggregation without loss.
minor comments (1)
  1. [Abstract] Abstract contains a typographical error: 'predicatesas' should be 'predicates as'.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive and detailed feedback. The comments highlight important gaps in the current presentation that we will address through revision. We respond to each major comment below.

read point-by-point responses

  1. Referee: [Abstract] Abstract: the unification and type system are asserted without any formal semantics, typing rules, derivations, or even small examples of how graded effects check grounding or how relevance types interact with higher-order functions; the central claim therefore cannot be verified from the provided text.

    Authors: We agree that the manuscript asserts the unification of functional and logic programming via finitely supported functions and sketches a type system using graded effects and relevance types, but does so without supplying formal semantics, complete typing rules, derivations, or concrete examples. This limits verifiability of the central claims from the text. In the revised manuscript we will add a formal semantics for finitely supported functions over pointed sets, explicit typing rules for the graded effects (to enforce grounding) and relevance types (to model the zero element), example type derivations, and small examples showing their interaction with higher-order functions. revision: yes

  2. Referee: [Abstract] Abstract: the weakest assumption—that finitely supported functions over pointed sets preserve the full semantics and expressiveness of logic programming without additional mechanisms—is stated but not demonstrated; no argument is given showing that the representation as input-output tables plus the proposed type system recovers standard Datalog operations or aggregation without loss.

    Authors: We accept this observation. The manuscript states that Datalog corresponds to finitely supported boolean functions representable as input-output tables and that generalization to other pointed sets handles aggregation and weighted logic programming, yet provides no explicit argument or demonstration that this representation plus the type system recovers the full expressiveness of standard Datalog operations and aggregation without loss or extra mechanisms. We will revise the paper to include a dedicated section containing an argument (with supporting examples) that the table representation together with the graded-effect and relevance-type discipline recovers standard Datalog operations such as joins and projections, as well as aggregation, without loss of expressiveness. revision: yes

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper's central move is a definitional unification: predicates are reinterpreted as functions equipped with their (finite) support, with Datalog as the boolean case and pointed-set generalization for aggregation. This is presented as a conceptual reframing rather than a derivation or prediction extracted from prior fitted results. The type system (graded effects for grounding, relevance types for pointed sets) is proposed to enforce the invariant, but no equations, parameters, or self-citations are shown to reduce the claimed unification back to its inputs by construction. The approach is self-contained as a modeling choice with no load-bearing self-referential steps.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 1 invented entities

Based on abstract only: the claim rests on the domain assumption that predicates are equivalent to functions with finite support and that pointed sets suffice for aggregation.

axioms (2)
  • domain assumption Predicates can be treated as functions equipped with their support without loss of semantics.
    Stated directly in the opening unification claim.
  • domain assumption Finitely supported functions can be represented as input-output tables.
    Explicit in the abstract as the representation mechanism.
invented entities (1)
  • Finite functional programming no independent evidence
    purpose: The combined paradigm of finitely supported functions as data with higher-order functions as code.
    New term and framing introduced to describe the unification.

pith-pipeline@v0.9.0 · 5381 in / 1280 out tokens · 34962 ms · 2026-05-07T13:37:56.711992+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

30 extracted references · 21 canonical work pages

  1. [1]

    Antoy,S.,Hanus,M.:Functionallogicprogramming.CommunicationsoftheACM53(4), 74–85 (Apr 2010)

    2010

  2. [2]

    In: Companion of the 2025 International Conference on Management of Data

    Aref, M., Guagliardo, P., Kastrinis, G., Libkin, L., Marsault, V., Martens, W., McGrath, M., Murlak, F., Nystrom, N., Peterfreund, L., Rogers, A., Sirangelo, C., Vrgoč, D., Zhao, D., Zreika, A.: Rel: A programming language for relational data. In: Companion of the 2025 International Conference on Management of Data. p. 283–296. SIGMOD/PODS ’25, Associatio...

    work page doi:10.1145/3722212.3724450 2025

  3. [3]

    In: Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming

    Arntzenius, M., Krishnaswami, N.R.: Datafun: A functional Datalog. In: Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming. pp. 214–

  4. [4]

    https://doi.org/10.1145/2951913

    ICFP 2016, ACM, New York, NY, USA (2016). https://doi.org/10.1145/2951913. 2951948

    work page doi:10.1145/2951913 2016

  5. [5]

    Augustsson, L., Breitner, J., Claessen, K., Jhala, R., Jones, S.P., Shivers, O., Jr., G.L.S., Sweeney, T.: The verse calculus: A core calculus for deterministic functional logic pro- gramming. Proc. ACM Program. Lang.7(ICFP), 417–447 (2023). https://doi.org/10. 1145/3607845

    2023

  6. [6]

    In: Pacholski, L., Tiuryn, J

    Benton, P.N.: A mixed linear and non-linear logic: Proofs, terms and models (extended abstract). In: Pacholski, L., Tiuryn, J. (eds.) Computer Science Logic, 8th International Workshop,CSL’94,Kazimierz,Poland,September25-30,1994,SelectedPapers.Lecture NotesinComputerScience,vol.933,pp.121–135.Springer(1994).https://doi.org/10. 1007/BFB0022251

    1994

  7. [7]

    In: Proceed- ings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, July 27-30, 1996

    Benton, P.N., Wadler, P.: Linear logic, monads and the lambda calculus. In: Proceed- ings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, July 27-30, 1996. pp. 420–431. IEEE Computer Society (1996). https://doi.org/10.1109/LICS.1996.561458

    work page doi:10.1109/lics.1996.561458 1996

  8. [8]

    In: Sabel, D., Thiemann, P

    Contrastin, M., Orchard, D.A., Rice, A.C.: Automatic reordering for dataflow safety of datalog. In: Sabel, D., Thiemann, P. (eds.) Proceedings of the 20th International Sym- posium on Principles and Practice of Declarative Programming, PPDP 2018, Frank- furt am Main, Germany, September 03-05, 2018. pp. 9:1–9:17. ACM (2018). https: //doi.org/10.1145/323695...

    work page doi:10.1145/3236950.3236954 2018

  9. [9]

    Reynolds

    Escardó, M.H.: Infinite sets that admit fast exhaustive search. In: 22nd IEEE Symposium on Logic in Computer Science (LICS 2007), 10-12 July 2007, Wroclaw, Poland, Pro- ceedings. pp. 443–452. IEEE Computer Society (2007). https://doi.org/10.1109/LICS. 2007.25

    work page doi:10.1109/lics 2007

  10. [10]

    Blog post (2007), https:// math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/

    Escardó, M.H.: Seemingly impossible functional programs. Blog post (2007), https:// math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/

    2007

  11. [11]

    Filardo, N.W.: Dyna 2: Towards a General Weighted Logic Language. Ph.D. thesis, Johns Hopkins University (10 2017), https://www.ietfng.org/nwf/publications-and-talks/ 2017-thesis.html Finite Functional Programming 17

    2017

  12. [12]

    Francis-Landau, M.: Declarative Programming via Term Rewriting. Ph.D. thesis, Johns Hopkins University (1 2024), https://matthewfl.com/research#phd

    2024

  13. [13]

    SIGPLAN Not.51(9), 476–489 (Sep 2016)

    Gaboardi, M., Katsumata, S.y., Orchard, D., Breuvart, F., Uustalu, T.: Combining effects and coeffects via grading. SIGPLAN Not.51(9), 476–489 (Sep 2016). https://doi.org/ 10.1145/3022670.2951939

    work page doi:10.1145/3022670.2951939 2016

  14. [14]

    In: Proceedings of the 21st ACM SIGPLAN International Con- ference on Functional Programming

    Gaboardi, M., Katsumata, S.y., Orchard, D., Breuvart, F., Uustalu, T.: Combining effects and coeffects via grading. In: Proceedings of the 21st ACM SIGPLAN International Con- ference on Functional Programming. p. 476–489. ICFP 2016, Association for Comput- ingMachinery,NewYork,NY,USA(2016).https://doi.org/10.1145/2951913.2951939, https://doi.org/10.1145/2...

    work page doi:10.1145/2951913.2951939 2016

  15. [15]

    Green,T.J.,Karvounarakis,G.,Tannen,V.:Provenancesemirings.In:Libkin,L.(ed.)Pro- ceedings of the Twenty-Sixth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, June 11-13, 2007, Beijing, China. pp. 31–40. ACM (2007). https: //doi.org/10.1145/1265530.1265535, https://doi.org/10.1145/1265530.1265535

    work page doi:10.1145/1265530.1265535 2007

  16. [16]

    (eds.) Proceedings Ninth Workshop on Mathematically Structured Func- tional Programming, MSFP@ETAPS 2022, Munich, Germany, 2nd April 2022

    Henglein,F.,Kaarsgaard,R.,Mathiesen,M.K.:Theprogrammingofalgebra.In:Gibbons, J., New, M.S. (eds.) Proceedings Ninth Workshop on Mathematically Structured Func- tional Programming, MSFP@ETAPS 2022, Munich, Germany, 2nd April 2022. EPTCS, vol. 360, pp. 71–92 (2022). https://doi.org/10.4204/EPTCS.360.4

    work page doi:10.4204/eptcs.360.4 2022

  17. [17]

    In: Proceed- ings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Lan- guages

    Katsumata, S.y.: Parametric effect monads and semantics of effect systems. In: Proceed- ings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Lan- guages. p. 633–645. POPL ’14, Association for Computing Machinery, New York, NY, USA (2014). https://doi.org/10.1145/2535838.2535846

    work page doi:10.1145/2535838.2535846 2014

  18. [18]

    Khamis, M.A., Ngo, H.Q., Pichler, R., Suciu, D., Wang, Y.R.: Convergence of datalog over (pre-) semirings. J. ACM71(2), 8:1–8:55 (2024). https://doi.org/10.1145/3643027

    work page doi:10.1145/3643027 2024

  19. [19]

    Publications de l’Institut Mathematique96, 17–23 (2007)

    Kosta, D., Petrić, Z.: Relevant categories and partial functions. Publications de l’Institut Mathematique96, 17–23 (2007). https://doi.org/10.2298/PIM0796017D

    work page doi:10.2298/pim0796017d 2007

  20. [20]

    Kovach, S., Kolichala, P., Gu, T., Kjolstad, F.: Indexed streams: A formal intermediate representation for fused contraction programs. Proc. ACM Program. Lang.7(PLDI) (Jun 2023). https://doi.org/10.1145/3591268

    work page doi:10.1145/3591268 2023

  21. [21]

    Madsen, M., Lhoták, O.: Fixpoints for the masses: programming with first-class data- log constraints. Proc. ACM Program. Lang.4(OOPSLA) (Nov 2020). https://doi.org/10. 1145/3428193

    2020

  22. [22]

    O’Hearn, P.W., Pym, D.J.: The logic of bunched implications. Bull. Symb. Log.5(2), 215– 244 (1999). https://doi.org/10.2307/421090

    work page doi:10.2307/421090 1999

  23. [23]

    In: Ali, K., Vitek, J

    Pacak, A., Erdweg, S.: Functional programming with Datalog. In: Ali, K., Vitek, J. (eds.) 36th European Conference on Object-Oriented Programming, ECOOP 2022, Berlin, Ger- many, June 6-10, 2022. LIPIcs, vol. 222, pp. 7:1–7:28. Schloss Dagstuhl - Leibniz- Zentrum für Informatik (2022). https://doi.org/10.4230/LIPICS.ECOOP.2022.7

    work page doi:10.4230/lipics.ecoop.2022.7 2022

  24. [24]

    Stud Logica70(2), 271–296 (2002)

    Petrić, Z.: Coherence in substructural categories. Stud Logica70(2), 271–296 (2002). https://doi.org/10.1023/A:1015186718090

    work page doi:10.1023/a:1015186718090 2002

  25. [25]

    In: Jeuring, J., Chakravarty, M.M.T

    Petricek, T., Orchard, D.A., Mycroft, A.: Coeffects: a calculus of context-dependent computation. In: Jeuring, J., Chakravarty, M.M.T. (eds.) Proceedings of the 19th ACM SIGPLAN international conference on Functional programming, Gothenburg, Sweden, September 1-3, 2014. pp. 123–135. ACM (2014). https://doi.org/10.1145/2628136. 2628160

    work page doi:10.1145/2628136 2014

  26. [26]

    Raedt, L.D., Kimmig, A., Toivonen, H.: Problog: A probabilistic prolog and its application inlinkdiscovery.In:Veloso,M.M.(ed.)IJCAI2007,Proceedingsofthe20thInternational Joint Conference on Artificial Intelligence, Hyderabad, India, January 6-12, 2007. pp. 2462–2467 (2007), http://ijcai.org/Proceedings/07/Papers/396.pdf 18 Arntzenius and Willsey

    2007

  27. [27]

    Lang.9(PLDI), 1220–1244 (2025)

    Rioux,N.,Zdancewic,S.:Functionalmeaningforparallelstreaming.Proc.ACMProgram. Lang.9(PLDI), 1220–1244 (2025). https://doi.org/10.1145/3729299

    work page doi:10.1145/3729299 2025

  28. [28]

    Shaikhha, A., Huot, M., Smith, J., Olteanu, D.: Functional collection programming with semi-ring dictionaries. Proc. ACM Program. Lang.6(OOPSLA1), 1–33 (2022). https: //doi.org/10.1145/3527333

    work page doi:10.1145/3527333 2022

  29. [29]

    Journal of Mathematical Sci- ences151, 3032–3051 (6 2008)

    Smirnov, A.L.: Graded monads and rings of polynomials. Journal of Mathematical Sci- ences151, 3032–3051 (6 2008). https://doi.org/10.1007/s10958-008-9013-7, trans- lated from Zapiski Nauchnykh Seminarov POMI, Vol. 349, 2007, pp. 174–210

    work page doi:10.1007/s10958-008-9013-7 2008

  30. [30]

    Somogyi, Z., Henderson, F., Conway, T.C.: The execution algorithm of mercury, an effi- cient purely declarative logic programming language. J. Log. Program.29(1-3), 17–64 (1996). https://doi.org/10.1016/S0743-1066(96)00068-4

    work page doi:10.1016/s0743-1066(96)00068-4 1996