HTTPS SSH

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:

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.

  4. If there are holes remaining, jump to step 1.

  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.