In tribute to Lawvere, here is one of his ideas that is simple enough to explain in one post.

The original paper is "Diagonal arguments and cartesian closed categories" (http://tac.mta.ca/tac/reprints/articles/15/tr15abs.html)

Lawvere's fixed point theorem is the positive constructive content of many diagonalization arguments.

Here I'll show how it unifies Cantor's theorem that there's no surjection from a set to its powerset and the construction of the Y combinator.

Lawvere's fixed point theorem in type theory:

If r : X -> (X -> D) is surjective (forall f: X -> D. exists x. r x = f), then for every function h : D -> D there exists d : D. a fixed point of h , i.e., h d = d.

Proof:

Given h : D -> D, by surjectivity there exists l:X such that r l = λ x. h(r x x).

Then r l l is a fixed point of h:

r l l = (λ x. h(r x x)) l = h (r l l)

Corollary: Cantor's theorem. There is no surjection X -> (X -> Prop).

Proof:

If there were, then every h : Prop -> Prop would have a fixed point, but not : Prop -> Prop does not have a fixed point (exercise).

If we strengthen the hypothesis we can get something which makes sense purely in the equational theory of the lambda calculus (i.e., no existential quantifiers) and therefore interpretable in all Cartesian Closed Categories.

Variant of Lawvere's fixed point theorem in STLC:

if r : X -> (X -> D) is a retract of s : (X -> D) -> X (i.e., (λ x. r(s(x))) = (λ x. x)), then we can construct a fixed point combinator Y : (D -> D) -> D, i.e., Y = λ h. h(Y h).

Note that in the presence of the axiom of choice, this variant is equivalent to the previous, but the most interesting applications are in settings without choice.

Proof:

Y = λ h. r (s (λ x. h(r x x))) (s (λ x. h(r x x)))

Here s (λ x. h(r x x)) is the l in the previous proof, where our strengthened hypothesis gives us a choice of element rather than its mere existence.

Then

Y

= λ h. Y h

= λ h. r (s (λ x. h(r x x))) (s (λ x. h(r x x)))

= λ h. (λ x. h(r x x)) (s (λ x. h(r x x)))

= λ h. h(r (s (λ x. h(r x x))) (s (λ x. h(r x x)))))

= λ h. h(Y h)

Which is the Y combinator in STLC, which more typically is constructed using a recursive type X =~ (X -> D) with r, s the isomorphism, or in untyped lambda calculus which is equivalent to having a single type D where if only β is assumed then D is a retract of (D -> D) and with η then D is isomorphic to (D -> D).

Related expository material:

- https://arxiv.org/abs/math/0305282

- https://math.andrej.com/2007/04/08/on-a-proof-of-cantors-theorem/

- https://www.cs.bham.ac.uk/~mhe/agda-new/LawvereFPT.html

The notion of model of intuitionistic propositional logic (IPL) I'm

most familiar with (being a category theory/PL nerd) is a Heyting

algebra (HA): a poset with finite meets, finite joins and a Heyting

implication. If you add propositional variables, the model includes a

choice of how to interpret them as elements of the HA and if you

include axioms, their interpretation must be true in the HA.

Then you can interpret every proposition of IPL as an element of the

HA where you interpret conjunctions as meets, disjunctions as joins

and implication as the Heyting implication. If G |- A is provable then

/\ [G] |- [A] is true.

If you look up what a model of IPL is though, you'll likely find

Kripke models, and they look at first a bit different: It's a pair of

a poset W, and a "forcing relation" ||- between elements of W and

propositions of IPL satisfying a bunch of properties:

1. for variables x, if w ||- x and v <= w then v ||- x

2. w ||- p /\ q iff w ||- p and w ||- q

3. w ||- true is true

4. w ||- p \/ q iff w ||- p or w ||- q

5. w ||- false is false

6. w ||- p => q iff for any v <= w if v ||- p then v ||- q

Despite the cosmetic difference, Kripke models are instances of the HA

model construction. Given a poset W, the HA in question is

Prop^(W^op), the poset of antitone functions from W to Prop

(classically, Prop is just the boolean order 0 <= 1). This has the

pointwise ordering: f <= g if for every w. f w implies g w.

This is a Heyting Algebra:

top w iff true

(f /\ g) w iff f w and g w

bot w iff false

(f \/ g) w iff f w or g w

(f => g) w iff for any v <= w. if f w then g w

Then an interpretation of the propositional variables in this HA would

be an assignment for each variable X and w a proposition [x] w that is

antitone in w: if [x] w and v <= w then [x] v. Then the model HA

interpretation defines exactly our Kripke forcing semantics. It

defines for each proposition of IPL p a function from W to Prop that

is antitone, i.e., [p] : W^op -> Prop. Then the definition of Kripke

model is just an infix notation for this semantics:

w ||- p := [p] w

And if you unravel the definitions of the HA semantics and the HA

structure of the poset, you reproduce exactly the definition of a

Kripke model.

Bonus: this is all a "de-categorification" of a similar situation for

lambda calculus. The Kripke models are presheaf categories and the HA

are bi-cartesian closed categories.

“Compiling higher-order specifications to SMT solvers” slides and link paper: https://bentnib.org/posts/2023-01-17-higher-order-specs-to-smt.html

A last-minute-COVID-forced remote talk about type based analyses for checking and translating higher-order specifications to SMT solvers.

Catala is a programming language for the law. It has a feature for making definitions with defaults and overrides. I think the description in the Catala ICFP paper hides how elegant and simple this is.

A simple semantics for defaults in Catala: https://bentnib.org/posts/2023-01-16-catala.html

Data types with Negation -- some slides from a talk about how to understand data type definitions that include negation.

The talks were a while ago, but I never put the slides online anywhere.

https://bentnib.org/posts/2023-01-15-datatypes-with-negation.html

By the way, js_of_ocaml 5.0 has been released with (opt-in) support for effect handlers 🙂 https://discuss.ocaml.org/t/ann-js-of-ocaml-5-0/11008

js_of_ocaml is a compiler from OCaml to Javascript. It allows to do a number of cool things such as the OCaml Playground https://ocaml.org/play or Learn OCaml https://ocaml-sf.org/learn-ocaml-public/#

All credit where credit is due, the effect support in js_of_ocaml uses a CPS transform adapted from the one proposed by Daniel Hillerström, @reifyreflect, @bentnib and @kayceesrk

in “Continuation Passing Style for Effect Handlers” and “Effect handlers via generalised continuations”!

Can't wait to be back in Paris this late April thanks to my upcoming ESOP paper: 'Builtin Types viewed as Inductive Families' https://gallais.github.io/pdf/esop23-thin.pdf

Category Theory, Presheaves, Long Explanation

The usual definition of a presheaf P on a category C is a functor C^op -> Set. But here is a more conceptual way to think about it. (For the experts, basically it’s the same idea as a monoid/group action).

First, a category is a notion of object and morphism between objects. These morphisms can be composed if the source of one matches the target of the other. I.e., they can be composed “tip to tail”. You need identity morphisms for this composition and the composition is associative. This all justifies notation like drawing morphisms by concatenating arrows without using parentheses (picture 1). Or writing a composition as `f;g;h` or even `hgf` with just concatenation.

One way to think about a presheaf P on a category C is that it extends the notion of morphism. We had morphisms with a source and target, and the presheaf defines a new notion: a morphism that has a source but no target. What kind of composition should such a thing have? Well if I have a morphism f with domain A and codomain B and I have a morphism phi with domain B but no codomain, then I should still be able to compose them together to get a morphism with domain A and no codomain. That is, we can compose these “morphisms to nowhere” with ordinary morphisms on one side but not the other (since there is no codomain object to tell us what kind of morphisms we can compose with). This kind of composition should intuitively extend the existing notion: composing an arrow with no codomain with the identity (id; phi = phi) shouldn’t change it and there should be an Associativity when combining with ordinary composition (f;g);phi = f;(g;phi). These rules make it so that we can cleanly extend our original notation for composition to these new morphisms (picture 2). It is a very useful exercise to figure out why this data is precisely the same as a functor from C^op to Set.

A few observations:

1. This all would work perfectly fine with arrows that only have a codomain and no domain. These are “copresheaves” and are equivalent to functors C to Set.

2. For any object A of C, we could define a presheaf by defining an arrow with no codomain to be an arrow into A! Then this satisfies the right identity and Associativity rules because it is just ordinary composition. This construction turning an object of a category into a presheaf on it is the Yoneda embedding!

3. Once we have seen (2) we should ask for any presheaf: Is this notion of morphisms with no codomain really just the same as morphisms into some fixed object? If it is, then we call it a *representable* presheaf.

The concept of a representable presheaf is, in my opinion, the most important idea of category theory. It deserves more in another post but here’s just one example that I learned from Emily Riehl’s textbook (Category Theory in Context) to tie everything together. Take the category of (undirected) graphs and graph homomorphisms. A K-coloring of a graph is an assignment of a number [1,…K] for each vertex of a graph such that if two vertices are connected by an edge, they have to be assigned different colors. The concept of a K-coloring turns out to be a presheaf. We can think of a K-coloring of a graph G as a morphism chi with domain G but no codomain. If I have a graph homomorphism f from H to G, then I can compose the coloring chi with f to get a coloring f;chi on H (since homomorphisms preserve adjacency) and this satisfies the correct identity and associativity rules. Once we realize this we should ask: is this notion representable? I.e., is there a special graph Q(K) such that a K-coloring on G is the same thing as a homomorphism from G to Q(K)? I’ll post the answer in a reply.

New website design for a new year: https://bentnib.org/

- Website
- https://bentnib.org/

Joined Apr 2022