Bob Atkey boosted

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

Bob Atkey boosted
Bob Atkey boosted

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

youtube.com/watch?v=LFilYalaF9

Bob Atkey boosted

🧵 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)

ArXiv is great for lots of reasons, but the main one for me is that it doesn't open a new fucking tab every time you breathe.

Bob Atkey boosted

Our paper on the cumulative hierarchy and ordinals in HoTT got accepted at LICS! 🎉
arxiv.org/abs/2301.10696

Bob Atkey boosted

I'm overjoyed to announce that I will be starting as an Associate Professor in Logical Foundations and Formal Methods at University of Cambridge this fall!

Bob Atkey boosted

is it just me or are lights brighter when it's louder

Using `unsafeCoerce` (or `Obj.magic`) is like standing up during a theatre performance and sternly shouting "You're all liars! You aren't who you're pretending to be!"

Is it true?

Is it helpful?

Bob Atkey boosted

I handed in my thesis!

people.compute.dtu.dk/ahfrom/ahfrom-thesis.pdf

Bob Atkey boosted

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" (tac.mta.ca/tac/reprints/articl)

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:
- arxiv.org/abs/math/0305282
- math.andrej.com/2007/04/08/on-
- cs.bham.ac.uk/~mhe/agda-new/La

Tested negative! Just in time for POPL to be over!

Every time the session chair at POPL says "Remember to say your name and your affiliation" I just think of Bruce Forsyth on the Generation Game asking "What's your name and where're you from?"

Bob Atkey boosted

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.

Every Virtual Learning Environment expands until it has a bug ridden unusable half implemented spreadsheet for incorrectly computing final marks.

I should've gone to Boston, Lincolnshire. Would've been substantially cheaper and I wouldn't be jetlagged.

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

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

Show older
types.pl

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.