I often find at work I wish I could say: Just let me write a SELECT query against your backend databases. I can make this problem go away and save several FTEs work faffing around manually with spreadsheets... #Databases #SingleSourceOfTruth #AcademicIT

this video is making a lot of things about how conversation work click into place for me for the first time

also, why responding to long emails is hard

🧵 Thread: Genuine quotes from experts and eyewitnesses on Arthur C. Clarke's Mysterious World (1980), a British television series which looked at unexplained phenomena from around the world.

#supernatural #paranormal #occult #psychic #UFOs #ghosts #yeti #cryptozoology

(originally posted on the bird site)

Our paper on the cumulative hierarchy and ordinals in HoTT got accepted at LICS! 🎉

https://arxiv.org/abs/2301.10696

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.

- Website
- https://bentnib.org/

- Location
- Edinburgh

Joined Apr 2022