# Overview

## 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
next(state) := if state = ready & request = TRUE

• 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:

Emacs usage:

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:

1. Go into a hole (these can be created using ? or {!!}), and click C-c C-,. This shows what is the Goal and what are the assumptions we already know (under the horizontal line ----).

Instead of C-c C-, you can use C-u C-u C-c C-,-t, this unfolds all the abbreviations when writing the goal and the assumptions.

2. Write some proof, press C-c 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 become X → X or Y → Y. _123 → _124 can become X → Y vagy Y → X or even X → X etc.

How do you write a proof?

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

2. 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 → ?.

1. 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 a p : X → Y, you can write p ?.

3. If Goal: is the same as Have: (or a special case of it through specialisation of metavariables), you can accept what you have written in the goal by: C-c C-space.

5. You can reload the file by C-c C-l.

## 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 C-c C-n (for normalisation).

## Peano arithmetic

Rules for natural numbers:

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

• zero : ℕ

• if n : ℕ, then suc n : ℕ

• if n : ℕ, C : Set, a : C, f : C → C, then

• rec 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, then a ≡ b is a type. Elements of a ≡ b are proofs of equality of a and b.

• To construct proofs of equality, one can use the following:

• refl a : a ≡ a

• if p : a ≡ b, then sym p : b ≡ a

• if p : a ≡ b and q : b ≡ c, then trans p q : a ≡ c

• if f : A → B, a : A, b : A and p : a ≡ b, then cong f p : f a ≡ f b

Universal quantification:

• (n : ℕ) → n + zero ≡ n is the type which says that for all n, n + zero is equal to n.

• (x : A) → B is a generalisation of A → B where x can appear in B. The rules are the following:

• if, given x : A, we have t : B, then λ x → t : (x : A) → B

• for example, (λ n → refl n) : (n : ℕ) → zero + n ≡ n
• if f : (x : A) → B and u : A, then f u : B[x ↦ u]

• for example, if f : (n : ℕ) → n + zero ≡ n, then f (suc zero) = (n + zero ≡ n)[n ↦ suc zero] = (suc zero + zero ≡ suc zero)

Predicates and relations:

• a P : A → Set is called a predicate on A or a family of types indexed over A

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

• an R : A → A → Set is called a binary relation on A

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

• the eliminator for equality:

• if P : A → Set, q : a ≡ b, u : P a, then subst P q u : P b

Induction on natural numbers:

• if n : ℕ, P : ℕ → Set, z : P zero, s : (n : ℕ) → P n → P (suc n), then

• ind 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 an A such that P is true for it.

• if a : A, b : P a, then a ∙ b : Σ A b (write as \.)

• if w : Σ A P, then pr₁ w : A and pr₂ w : P (pr₁ w)

• pr₁ (a ∙ b) = a and pr₂ (a ∙ b) = b

Decidability.