You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
William Oakcraft (Aug 28 2026 at 16:31):Good morning!
I want to give complete context for my question as for me it seems somewhat specific as I've received many unhelpful suggestions, so for those who prefer you should skip to the [QUESTION] label. I ask your pardon for my longwindedness.
My long time research pursuits have been in the so called "pointfree calculation" in formal methods of specification and refinement in computer science (the Algebra of Programming/Bird-Meertens/Squiggol tradition common in Belgium, the Netherlands and Portugal), relational methods and their pedagogical use for teaching mathematics (made popular by authors such as Gunther Schmidt ). This style can be traced back to Peirce/Schroder and Tarski's relation calculus/algebras and Freyd/Scedrov's allegories, but there is also much work in their use in algebraic logic and proof theory through Ewa Orlowska school, fork algebras and also very interesting studies of these styles in formal semantics of natural languages per Michael Bottner
and Renate Schmidt.
As my main interests are in the development of pedagogical formal and intuitive tools for the practical scientist (either in CS, pure mathematics or other applied sciences) for abstract requirement specification and stepwise refinement down to proofs, concrete examples and implementation, I would ideally like to assemble a formalism stack in which 1) the most abstract level would be general and broadly applicable as possible (thus with as little existential import/requirements - as thus as partial - as possible) and one could step by step get the high-level specification more proof-relevant and with more computational content in the intermediate levels, 2) one could have seemingly uniform proof procedures/calculational rules all throughout these systems (uniform in the sense of being able to have similar algebraic visual representations), 3) the user would have to deal as little as possible with non-essential implementation details (such as variable binding and substitution metatheory or generally analytic set-theoretic metatheory questions which aren't of much use in the more synthetic/structural frameworks I prefer) and 4) however, making clearly explicit some other computational details which are sadly most of the times left implicit but which would clarify better the semantics (theory vs metatheory, mention and use, intensionality and extensionality - in the case of function and predicate/relation symbols -, choice principles and explicit structural rules-resource management - so more towards substructural/linear logics and types - I've seen this has been a question for a long time in formal methods and automated metatheory, as seen in use/mention notational distinctions in the Z language and Raymond Boute's Functional Mathematics or Paul Gilmore's intensional type theories).
Unfortunately, in most type-theoretical tradition I have found immediate obstacles to this ideal: from my understanding, the strive for Cartesian typing contexts and traditional lambda calculi-style management of variables and substitution metatheory (as well as the central role of lambda application and abstractions instead of composition + explicit management of resource duplication and contraction) leads to the asymmetry in the treatment of functions (the single-valued and singular-term bias) vs relations/multi-valued/set-valued functions, privileging the treatment of the former (and thus leading to the stereotypical "functional" language - as in "there exists a morphism such that..." instead of a more natural relational terminology) for the handicap of the latter. This seems to be somewhat of a big deal when dealing with at the same time explicit (thus not relying on tactics as in current Lean culture) but natural/accessible/intuitive and general specification and refinement formalisms, as you can't naturally make a very general specification which returns a wide interval of results and later only refine it to the desired interval: you are forced to encode this in the functional lingo of these formalisms, which I am not sure is natural for most people. This seems also bad for dealing with stateful and more nondeterministic use cases, and from my teaching experience in logic and functional programming dealing with the complex variable binding, renaming and substitution metatheory of lambda calculus and FOL is one of the main barriers for students to really enjoy doing formal proofs in these frameworks (also, and it's a main argument in the works in "Natural Logic" by Lawrence Moss, this does not resemble at the slightest natural language proofs' structure).
[QUESTION] I have currently found many frameworks which could be useful to that objective such as virtual equipments, Kleisli categories, multicategories and polycategories, spans, regular and coherent logic but also Dialectica/Chu categories and general realizability/Kohlenbach-style proof mining for the "refinement" intermediate parts as well as some lambda-free logical frameworks papers by Altenkirch and others in automatized metatheory works, however as there is much literature to review (and I am not in a very categorical/type-theoretical-methods-heavy institute and university so usually I don't have much people to talk about these topics) could someone give me general tips and some directions I should go towards and other directions I should not giving these preferences of mine? (for reminder: pointfree/variable-free and compositional formalisms, not having to deal with lambda calculi's substitution metatheory, explicit resource management/substructural contexts, putting relations in a central role and functional relations as only special cases - as well as choice principles for getting functions out of them explicit - such as the relational power transpose - and maybe even removing the asymmetry of singular element images of single-valued functions vs set/plural/set element images of multi-valued functions and relations entirely by making function/relation images structural/"black box" by default in some way?).
I think one central aspect of my doubts seem to be how much "stratified" term/type structures (the stratification inherent to membership relations and lambda application - and thus the definite term-type separation of MLTT-style type systems - in counterpart to inclusion/partial orders and compositions everywhere) are essential to the good simplifying and computational properties of contemporary popular category theory and type theory frameworks. In set-theoretic mathematics and set-theoretic-influenced relational methods one can just manipulate domains and images of functions/relations as any other term, the term-type structure is flattened/cumulative and everything can be just manipulated inside equations. That way, it seems that one can formulate the difference between single and multivalued functions/relations as just one of cardinality of element-images (or, structurally, well-behaving algebraic manipulation properties such as having coreflexive compositions of the inverse of a function and itself - and reflexive and coreflexive/identical in the case of isomorphisms). From my experience, students and practical scientists/engineers/programmers find this much more intuitive to work with, but when dealing with more traditional category theory and type theory works they are immediately forced to encode everything in a more idiosyncratic language and syntax.
For context, I have more experience in classical/set-theoretic style logic (especially proof theory and model theory) and some categorical logic to the level of the first few chapters of Bart Jacobs's book and Maclane's SGL; I have been currently trying to get up to pace with higher categories through the recent Cisinski/Cnossen et all Synthetic Category Theory book project and Leinster's Higher Operads, Higher Categories. My experience with dependent type theories is more informal through Lean and Agda and informal introductions such as the HoTT book and Marc Bezem et al's Symmetry and with type theories in general through Nederpelt and Geuvers's Type Theory and Formal Proof and Barendregt's Lambda Calculus with Types.
I again ask your pardon for my longwindedness and appreciate your replies.
Patrick Nicodemus (Aug 29 2026 at 19:53):I have one point of confusion.
https://adam.chlipala.net/cpdt/cpdt.pdf
Chapter 13 of this book talks about the use of inductively defined relations as specifications, and talks about writing tactics to prove theorems about them. You can prove theorems using this, and then gradually refine your specification until it describes the exact graph of a function. So I don't see what you mean by 'the type theoretic formalism requires you to start with a function.' You can use relations to your heart's content. I guess you're saying that at some point in the refinement of the specification you have to switch to writing a lambda function, and that's a qualititative break in the 'kind' of thing you're talking about, and that's what you're trying to avoid.
Maybe that specification happens to be executable. You said you have taught logic programming, so you have a good idea of what an executable specification looks like. But you do have to specify a specific sublanguage of relational logic for doing logic programming, and prove that your specification is equivalent to one in that framework/sublanguage.
We have many notions of an algorithm or a model of computation - Turing machines, lambda calculus, Warren abstract machine, whatever. But at the end of the day if you want to write code, you have to 'write code' for a model of computation. And that feels like something qualitatively different to me than defining a relation which is provably single-valued. Even in the logic programming context, you know, to me it's not realistic or even desirable to abstract away from the execution semantics. Maybe if you have a logic programming language where all programs terminate, I would buy it.
Am I on the right track here? are you looking for some semantics of logic programming?
Patrick Nicodemus (Aug 29 2026 at 19:54):It feels like maybe you just want a theorem prover based on logic programming. Abella -https://abella-prover.org/
Beluga - https://beluga-lang.readthedocs.io/en/latest/harpoon/prover-structure.html
Twelf is based on logic programming, not sure if it's really maintained anymore
Patrick Nicodemus (Aug 29 2026 at 19:58):I would also say that programming without variables and messiness with variable binding rules seems like combinatory logic. You didn't mention combinatory logic in your post, but maybe you're interested in papers on combinatory programming languages and proving correctness theorems about languages based on combinators? Certainly that seems like it would accomplish the basic goal of getting rid of messy variable binding and substitution rules, but I'd hazard a guess that it has its own complexities.
Patrick Nicodemus (Aug 29 2026 at 20:02):(I find it difficult to imagine writing a large program in a way that breaks with the tradition of defining functions within a module or class by a name, and referring to those functions from other modules by the same name. I think point-free programming works sense for individual functions, but I can't really wrap my head around a point-free system of modules, classes, and function definitions. So I suspect name bindings and name scoping issues are always going to be around at the macro level even if people start writing their individual functions in a point-free style.)