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
2
What is Intuitionistic Logic?
Intuitionistic Logic Correction Administrivia
3
What is Intuitionistic Logic?
Classical logic is the logic that most people know about.
Intuitionistic Logic Correction Administrivia
4
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.
Intuitionistic Logic Correction Administrivia
5
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 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.
6
Intuitionistic Logic Correction Administrivia
7
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).
Intuitionistic Logic Correction Administrivia
8
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:
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
9
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
10
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
11
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
12
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
13
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
14
Intuitionistic Logic Correction Administrivia
Translating
We can translate logical connectives to types and back:
Conjunction (∧) Disjunction (∨) Implication True
False
Tuples
Either
Functions
() Void
15
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)
16
TrafficLight
Red
Amber
Green
≃ Either () (Either () ())
≃ Left()
≃ Right (Left ())
≃ Right (Right (Left ()))
Intuitionistic Logic Correction Administrivia
Type Correctness
Γ ⊢ e :: A Γ ⊢ e :: B
Γ ⊢ () :: () () Γ ⊢ Left e :: Either A B SL Γ ⊢ Right e :: Either A B SR
17
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
18
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
19
Intuitionistic Logic Correction Administrivia
20
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
21
Wrap-up
1 Assignment 2 is before my next lecture (5th August).
Intuitionistic Logic Correction Administrivia
22
Wrap-up
1 Assignment 2 is before my next lecture (5th August).
2 There is a quiz for this week, but no exercise.
Intuitionistic Logic Correction Administrivia
23
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.
Intuitionistic Logic Correction Administrivia
24
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.
Intuitionistic Logic Correction Administrivia
25
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
26
Consultations
Consultations will be made on request. Ask on piazza or email cs3141@cse.unsw.edu.au.
Intuitionistic Logic Correction Administrivia
27
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.
Intuitionistic Logic Correction Administrivia
28
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.
Intuitionistic Logic Correction Administrivia
29
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.