Overview
Atlassian Sourcetree is a free Git and Mercurial client for Windows.
Atlassian Sourcetree is a free Git and Mercurial client for Mac.
What is this course about?
Ways to make sure a program is correct:

running the program with different inputs and checking that the outputs are as expected
Java JUnit framework

runtime monitoring
Exception in thread "main" java.lang.ArrayIndexOutOfBoundsException

simulation of a simplified model of the program and checking whether the model works as expected in all states of the simulated world
NuSMV
state : {ready, busy}, request : boolean init(state) := ready next(state) := if state = ready & request = TRUE then busy else {ready, busy}

partial specification of the program using types and checking whether the program matches this specification
4 : Int [1,2,4] : List Int (+) 4 : Int → Int length : String → Int "hello" : String length("hello") : Int

proving the program correct using formal methods
B method, Isabelle, Coq
In this course we focus on type systems.
Examples of types for the same program:
sort : List Int → List Int sort : List Int → SortedList Int sort : (xs : List Int) → (ys : SortedList Int) × (length xs = length ys) sort : (xs : List Int) → (ys : SortedList Int) × (length xs = length ys) × (x ∈ xs → x ∈ ys) sort : (xs : List Int) → (ys : SortedList Int) × (length xs = length ys) × (x ∈ xs ↔ x ∈ ys) sort : (xs : List Int) → (ys : SortedList Int) × (ys `permutationOf` xs)
Topics:

propositional logic

propositions as types

pattern matching
Goal:
 proving insertion sort correct
Examination:

weekly assignments, deadline next class

practical exam with Agda programming
Other:
 ask questions all the time
Setting up Agda
Installation:

http://people.inf.elte.hu/pgj/agda/tutorial/Installation.html

http://people.inf.elte.hu/reauaai/article/2017/02/15/atomagdapluginbeallitas.html
Emacs usage:

http://people.inf.elte.hu/pgj/agda/tutorial/Emacs_Usage.html

You can switch the Agda input mode on and off by
C\
. 
In Windows, you should use Dejavu Sans Mono font (the default font makes Emacs very slow).
Excercises:
git clone https://bitbucket.org/akaposi/agdaoktatas.git
Propositional logic
Propositional variables: X
, Y
, Z
.
Rules of propositional logic:
Introduction Elimination A B A × B A × B and _,_ proj₁ proj₂ A × B A B true tt ⊤ ⊥ false abort C A ⋮ B A → B A implies λ (space) A → B B A B A ⊎ B A → C B → C or inj₁ inj₂ case A ⊎ B A ⊎ B C
Notation:
proposition C 
prove C 
using an assumption p : C 
inputting 

A × B 
? , ? 
proj₁ p or proj₂ p 
\times , \_1 , \_2 
⊤ 
tt 
\top 

⊥ 
abort p 
\bot 

A → B 
λ a → ? 
p ? 
\ra , \Gl or \lambda 
A ⊎ B 
inj₁ ? or inj₂ ? 
case p ? ? 
\u+ , \_1 , \_2 
C 
p 
t : A
means that t
is a proof of proposition A
.
Abbreviations: ¬ A = A → ⊥
, A ↔ B = (A → B) × (B → A)
How to create proofs:

Go into a hole (these can be created using
?
or{!!}
), and clickCc C,
. This shows what is theGoal
and what are the assumptions we already know (under the horizontal line
).Instead of
Cc C,
you can useCu Cu Cc C,
t, this unfolds all the abbreviations when writing the goal and the assumptions. 
Write some proof, press
Cc C.
, this prints under the goal what proposition is proved by the proof you've written (Have:
).In the propositions you might see
_123
and similar metavariables, these can be replaced by anything, for example_123 → _123
can becomeX → X
orY → Y
._123 → _124
can becomeX → Y
vagyY → X
or evenX → X
etc.How do you write a proof?

If the goal is the same as one of the assumptions, you can simply give the assumption (last line of the table).

If the goal is a proposition created by one of the propositional connectives, you can use the operators in the second column (prove
C
) of the above table.
For example, if the goal is
X → Y
, you should writeλ x → ?
. If there are assumptions, you can use the third column (using
an assumption
p : C
) of the above table.
For example, if the goal is
Y
and you have ap : X → Y
, you can writep ?
. 

If
Goal:
is the same asHave:
(or a special case of it through specialisation of metavariables), you can accept what you have written in the goal by:Cc Cspace
. 
If there are holes remaining, jump to step 1.

You can reload the file by
Cc Cl
.
Propositions as types
So far, t : A
meant that t
is a proof of proposition A
. But
proofs can also be seen as programs and propositions as types. In this
view, t : A
means that the program t
has type A
.
For example, λ w → proj₁ w : X × Y → X
can be seen as a program
where the type of the input is X × Y
and the type of the output is
X
.
Dictionary:
our notation  usual programming  mathematics 

A × B 
record, multiple inputs  A*B 
⊤ 
unit, void (in C)  1 
⊥ 
empty type (uncommon)  0 
A → B 
function  Bᴬ 
A ⊎ B 
disjoint union, superclass of A and B 
A+B 
⊤ ⊎ ⊤ 
Bool  2 
⊤ ⊎ ... ⊎ ⊤ 
enum  1+...+1 
Types can be thought about as sets of programs/proofs. However there
is a difference from set theory: every program comes with its unqiue
type. This is why there is no union (∪
) operator. In set theory, we
have {0,1}∪{0} = {0,1}
, but {0,1}⊎{0} = {inj₁ 0, inj₁ 1, inj₂
0}
. If A
has 3 elements and B
has 2 elements, then A ⊎ B
has
3+2 elements, A × B
has 3*2 elements, A → B
has 2³ elements.
We can also run programs:

proj₁ (a , b) = a
,proj₂ (a , b) = b

(λ x → t) u = t[x ↦ u]
e.g.(λ w → proj₁ w) (tt , tt) = proj₁ (tt , tt)

case (inj₁ a) f g = f a
,case (inj₂ b) f g = g b
These can be seen as equalities of proofs as well. You can run
programs using Cc Cn
(for normalisation).
Peano arithmetic
Rules for natural numbers:

ℕ is a type
, we write this asℕ : Set

zero : ℕ

if
n : ℕ
, thensuc n : ℕ

if
n : ℕ
,C : Set
,a : C
,f : C → C
, thenrec a f n : C
rec a f zero = a
rec a f (suc n) = f (rec a f n)
This is how we can define addition, multiplication and other operations on natural numbers.
Rules for propositional equality:

if
A
is a type,a : A
,b : A
, thena ≡ b
is a type. Elements ofa ≡ b
are proofs of equality ofa
andb
. 
To construct proofs of equality, one can use the following:

refl a : a ≡ a

if
p : a ≡ b
, thensym p : b ≡ a

if
p : a ≡ b
andq : b ≡ c
, thentrans p q : a ≡ c

if
f : A → B
,a : A
,b : A
andp : a ≡ b
, thencong f p : f a ≡ f b
Universal quantification:

(n : ℕ) → n + zero ≡ n
is the type which says that for alln
,n + zero
is equal ton
. 
(x : A) → B
is a generalisation ofA → B
wherex
can appear inB
. The rules are the following: 
if, given
x : A
, we havet : B
, thenλ x → t : (x : A) → B
 for example,
(λ n → refl n) : (n : ℕ) → zero + n ≡ n
 for example,

if
f : (x : A) → B
andu : A
, thenf u : B[x ↦ u]
 for example, if
f : (n : ℕ) → n + zero ≡ n
, thenf (suc zero) = (n + zero ≡ n)[n ↦ suc zero] = (suc zero + zero ≡ suc zero)
 for example, if
Predicates and relations:

a
P : A → Set
is called a predicate onA
or a family of types indexed overA

example:
(λ n → n + two ≡ three) : ℕ → Set

an
R : A → A → Set
is called a binary relation onA

example: (λ x y → x ≡ y + three) : ℕ → ℕ → Set

the eliminator for equality:

if
P : A → Set
,q : a ≡ b
,u : P a
, thensubst P q u : P b
Induction on natural numbers:

if
n : ℕ
,P : ℕ → Set
,z : P zero
,s : (n : ℕ) → P n → P (suc n)
, thenind P z s n : P n
ind P z s zero = z
ind P z s (suc n) = s n (ind P z s n)
Rules for Σ
types (generalisation of ×
):

if
A : Set
,P : A → Set
,Σ A P : Set
. You can readΣ A P
as there exists anA
such thatP
is true for it. 
if
a : A
,b : P a
, thena ∙ b : Σ A b
(write as\.
) 
if
w : Σ A P
, thenpr₁ w : A
andpr₂ w : P (pr₁ w)

pr₁ (a ∙ b) = a
andpr₂ (a ∙ b) = b
Decidability.