[lou1306]

Some more food for thought on the meaning of =, from Girard's "Proofs and Types" [0]:

> There is a standard procedure for multiplication, which yields for the inputs 27 and 37 the result 999. What can we say about that? A first attempt is to say that we have an equality "27 x 37 = 999". This equality makes sense in the mainstream of mathematics by saying that the two sides denote the same integer [...] but it misses the essential point: There is a finite computation process which shows that the denotations are equal.

> [...] 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. The two expressions have different senses and we must do something (make a proof or a calculation, or at least look in an encyclopedia) to show that these two senses have the same denotation.

[0]: http://www.paultaylor.eu/stable/prot.pdf

[pron]

Just a bit of background: Girard is paraphrasing Frege's famous paper On Sense and Reference[1] which is an investigation into the meaning of equality. As a result of that investigation, Frege shows that terms in a language have at least two kinds of meanings (sense and reference or denotation), which Girard presents in a programming context.

[1]: http://www.scu.edu.tw/philos/98class/Peng/05.pdf

[cortesoft]

Oh man, I took a great class on that paper in college. Spent the whole quarter reading it, yet lecture was always interesting.

[jtc1983]

These quotes from Girard are great, as is the mention of Frege below.

Typically, the objects related by equality can be thought to have the same meaning with respect to extension and different meanings with respect to intension. Further, the difference in intension reveals something of the computational content of the extensional object being referred to.

Further topics to explore: the BHK interpretation of intuitionistic proof and the univalence axiom in homotopy type theory. Both of these topics give one some insight on the relationship between the computational content of mathematical objects and how this content pertains to the question of whether two objects are “the same.”

Finally, I did skim the article itself and found it lacking. The author seems to be aware of the fact that there are surprising, highly non-trivial properties of the (seemingly trivial) notion of equality in mathematics. And also to be aware of the fact that the use of ‘=‘ in CS contexts isn’t some sort of abuse of notation. But there seems to be very little of interest here beyond some circumstantial verification of these two general (and well-known) facts about equality in the mathematical and computational contexts.

[lou1306]

> Further topics to explore: the BHK interpretation of intuitionistic proof and the univalence axiom in homotopy type theory.

Thanks! For the interested, Girard's book focuses on the Curry-Howard isomorphism, another great result linking computer programs (actually, the typed lambda-calculus) to mathematical proofs.