Computational trinitarianism

Logic

Computational trinitarianism

Curry-Howard correspondence

• Conjunction <-> Pairs/product type
• Disjunction <-> Sum type
• Implication <-> function types
• Cut rule <-> substitution
• ...
• etc

Curry-Howard correspondence

• Proofs <-> programs
• Propositions <-> types
• Assumptions <-> variables/parameters
• MP <-> function application
• False <-> uninhabited type
• True <-> unit type

But why were we talking about programs?

*more scribbling on the board*

Additional connectives

~P = (P -> False)

sometimes questioned by the constructivists

Lambek's theorem

First rigorous logical system introduced by Arend Heyting

Intuitionistic logic

*scribble something on the board*

Curry-Howard isomorphism

Святая троица компьютерных вычислений

Intuitionistic logic

Brouwer-Heyting-Kolmogorov-interpretation

• "False" is not provable
• A proof of A&B consists of a proof of A and a proof or B
• A proof of A||B consists of a proof of A or a proof of B
• A proof of (A -> B) is a program that transforms a proof of A into a proof of B

Intuitionism

• Philosophical idea that mathematics is a creation of mind (anti-Platonism)
• Created by L.E.J. Brouwer
• Branch of "constructivism"

Constructive mathematics

The central dogma of computational trinitarianism holds that Logic, Languages, and Categories are but three manifestations of one divine notion of computation. There is no preferred route to enlightenment: each aspect provides insights that comprise the experience of computation in our lives.

- Robert Harper

For X to be true, we need to have a proof of X

Law of the excluded middle does not hold anymore

Alternatively: we don't care about truth(s), we only care about proofs

P or ~P

Relation to logic

But what does it mean for 'x' to be true?

x = True, y = True => x&y = True

x = True or y = True => x || y = True

Truth tables

Type systems

f = x + 2 :: Int, for every x :: Int

x :: A, y :: B => <x,y> :: (A,B)

=> f :: Int -> Int

Computer programs

• 4 :: Int
• "hello" :: String
• [1,2,3] :: List<Int>

(4+4) :: Int

("hello" <> " world") :: String

(4 + "foo") :: ???

Category theory

Hegelian logic

Category theory

More on category theory

William Lawvere is a mathematician and (arguably) a fan of Hegel's view on logic

Categories allow for many interesting constructions

Certain categories provide interpretation for type systems

Lawvere's work on CCCs and toposes:

internalization of logic -> objective logic

Many examples of concrete categories:

category of sets, category of monoids, category of groups, etc

• Elementary Theory of the Category of Sets
• Category of Categories as Foundations

Some objects can be viewed as "categories in small"

.. logic should be divided primarily into the logic of the Notion as being and of the Notion as Notion - or, by employing the usual terms <..> into 'objective' and 'subjective' logic..

• Category is a collection of objects and arrows
• Arrows go from one object to another
• Each object has an identity arrow
• Arrows can be composed

Programming

Category Theory

• Products
• Sums
• Initial objects
• Terminal objects

Lawvere's works are influenced by the Hegelian logic, in particular the Objective-Subjective division

Objects: types

Arrows: functions

- Categorical equivalent of a group

- Categorical equivalent of a monoid

- Etc

Cartesian Closed Categories

Thank you for listening!

Any questions?

Relevant literature:

• Bob Harper "The Holy Trinity"
• Andrei Rodin "Axiomatic Method and Category Theory"
• Per Martin-Loef "On the meaning of the logical constants and the justification of the logical laws"