T is for Types, not Sipping

By Scott

Hey everyone,

Friday night we discussed PFPL 46: Equality in System T. For those just joining in, System T is Goedel’s famous language which can be used to prove interesting properties, such as his yet more famous Incompleteness Theorem.

Next week we will be moving on to equality in richer climes in PFPL 47: Equality in PCF, meeting at the usual time and place, Friday at 6:30 at Gamma Space.

Equality like most obvious things is distressingly complex and difficult to define. I love this example from the opening of Girard’s book, Proofs and Types:

It is an abuse (and this is not cheap philosophy – it is a concrete question) to say that 27 x 37 equals 999, since if the two things we have were the same then we would never feel the need to state their equality. Concretely we ask a question, 27 x 37, and get an answer, 999.

This observation starts to unpack what it means when you write an equation on a blackboard. What rules are we implicitly applying in our minds to make sense of these lines and squiggles? When confronted with a requirement for clear definition, pinning down precise rules becomes quite a challenge and leads to the types of equational equivalences presented in this chapter.

In the case of functions, we use logical equivalence. When two functions evaluate to the same result on the same inputs, then we call them logically equivalent.

The opposing way of looking at this, is from the perspective of a program with a hole in it waiting for an expression. When for all possible program + holes (holy programs?) two expressions appear to be the same we call them observationally equivalent.

It’s remarkable that even in the context of system T, a complete and total language, when trying to compare two expressions the task seems to transform into something akin to a scientific process, where you have to perform experiments in order to validate your hypotheses.

All for now, happy computing, Scott