Intuitionistic Logic Correction Administrivia
1
Software System Design and Implementation
More on the Curry Howard Isomorphism
Curtis Millar
CSE, UNSW (and Data61) 29 July 2020
Intuitionistic Logic Correction Administrivia
What is Intuitionistic Logic?
Classical logic is the logic that most people know about.
Intuitionistic logic does not contain the axiom of excluded middle p ∨ ¬p or
equivalently ¬¬p → p.
In classical logic more can be proven but less can be expressed.
Intuitionistic proof of an existence statement gives a witness for the statement.
2
Intuitionistic Logic Correction Administrivia
Example of Existence in the Classical Sense
Let Q be the set of rational numbers and I be the set of irrational numbers. Considerthestatement∃x,y.(x∈I)∧(y∈I)∧(xy ∈Q).
Proof:
Consider the number
√ √2 2
√ √2
2 Otherwise if 2 ∈ I
.
√ √2
1 If 2 ∈Q
3
Intuitionistic Logic Correction Administrivia
Example of Existence in the Classical Sense
Let Q be the set of rational numbers and I be the set of irrational numbers. Considerthestatement∃x,y.(x∈I)∧(y∈I)∧(xy ∈Q).
Proof:
√ √2 Consider the number 2 .
√ √2
1 If 2 ∈Q√ √
Pickx= 2andy= 2 y √√2 y
Thenx =√2 sox ∈Q 2 Otherwise if √2 2 ∈ I
4
Intuitionistic Logic Correction Administrivia
Example of Existence in the Classical Sense
Let Q be the set of rational numbers and I be the set of irrational numbers. Considerthestatement∃x,y.(x∈I)∧(y∈I)∧(xy ∈Q).
Proof:
√ √2 Consider the number 2 .
√ √2
1 If 2 ∈Q√ √
Pickx= 2andy= 2 y √√2 y
Thenx =√2 sox ∈Q
2 Otherwise if √2 2 ∈ I
√ √2 √
Pickx= 2 andy= 2
y√√2√2√2 y Thenx=(2 ) = 2=2sox∈Q
5
Intuitionistic Logic Correction Administrivia
Recall: The Curry-Howard Isomorphism
This correspondence goes by many names, but is usually attributed to Haskell Curry and William Howard.
It is a very deep result:
Logic
Programming
Propositions Proofs
Proof Simplification
Types Programs Evaluation
It turns out, no matter what logic you want to define, there is always a corresponding λ-calculus, and vice versa.
Constructive Logic Classical Logic Modal Logic Linear Logic Separation Logic
Typed λ-Calculus Continuations Monads
Linear Types, Session Types Region Types
6
Intuitionistic Logic Correction Administrivia
Translating
We can translate logical connectives to types and back:
Conjunction (∧) Disjunction (∨) Implication True
False
Tuples
Either
Functions
() Void
7
We can also translate our equational reasoning on programs into proof simplification on proofs!
Intuitionistic Logic Correction Administrivia
Constructors and Eliminators for Sums
data TrafficLight = Red | Amber | Green Example (Traffic Lights)
8
TrafficLight
Red
Amber
Green
≃ Either () (Either () ())
≃ Left()
≃ Right (Left ())
≃ Right (Right (Left ()))
Intuitionistic Logic
Correction Administrivia
Γ ⊢ () :: () ()
Γ ⊢ e :: A Γ ⊢ e :: B
Γ ⊢ Left e :: Either A B SL Γ ⊢ Right e :: Either A B SR
??? Left () :: ()
Type Correctness
Right (Left ()) :: Either () ()SR
Right (Right (Left ())) :: Either () (Either () ())SR
9
Intuitionistic Logic
Correction Administrivia
Γ ⊢ () :: () ()
Γ ⊢ e :: A Γ ⊢ e :: B
Γ ⊢ Left e :: Either A B SL Γ ⊢ Right e :: Either A B SR
() () :: ()
Right () :: Either () ()SR
Right (Right ()) :: Either () (Either () ())SR
Type Correctness
10
Intuitionistic Logic Correction Administrivia
11
Examples
prop_or_false :: a -> (Either a Void)
prop_or_false a = Left a
prop_or_true :: a -> (Either a ())
prop_or_true a = Right ()
prop_and_true :: a -> (a, ())
prop_and_true a = (a, ())
prop_double_neg_intro :: a -> (a -> Void) -> Void
prop_double_neg_intro a f = f a
prop_triple_neg_elim ::
(((a-> Void) -> Void) -> Void) -> a -> Void
prop_triple_neg_elim f a = f (\g -> g a)
Intuitionistic Logic Correction Administrivia
12
Wrap-up
1 Assignment 2 is before my next lecture (5th August).
2 There is a quiz for this week, but no exercise.
3 Next week’s lectures consist of an extension on dependent type systems and a revision lecture on Wednesday.
4 There will be a survey on Piazza for revision topics, comment on the poll with specific questions
5 If you enjoyed the course and want to do more in this direction, ask us for thesis topics, taste of research projects, and consider attending COMP3161 and COMP4161.
6 Fill in the myExperience reports, it is important for us to receive your feedback.
Intuitionistic Logic Correction Administrivia
13
Consultations
Consultations will be made on request. Ask on piazza or email cs3141@cse.unsw.edu.au.
If there is a consultation it will be announced on Piazza with a link a room number for Hopper.
Will be in the Thursday lecture slot, 9am to 11am on Blackboard Collaborate.
Make sure to join the queue on Hopper. Be ready to share your screen with REPL (ghci or stack repl) and editor set up.