HTTPS SSH

Miről szól ez a tantárgy?

Program helyes működésének biztosítása:

  • a program futtatása különböző bemenetekkel és a kimenetek ellenőrzése

    Java JUnit framework

  • a program futás idejű monitorozása

    Exception in thread "main" java.lang.ArrayIndexOutOfBoundsException
    
  • a program egy egyszerűsített modelljének szimulálása, és annak ellenőrzése, hogy a szimulált világ lehetséges állapotaiban megfelelő programműködést tapasztalunk -e

    NuSMV

    state : {ready, busy}, request : boolean
    init(state) := ready
    next(state) := if state = ready & request = TRUE
    then busy else {ready, busy}
    
  • a program részleges specifikálása típusokkal, és a program fordítása során ennek a specifikációnak való megfelelés ellenőrzése

    4 : Int
    
    [1,2,4] : List Int
    
    (+) 4 : Int  Int
    
    length : String  Int
    
  • a program helyességének bizonyítása formális eszközökkel vagy bizonyítottan helyes program szintézise

    B módszer, Isabelle, Coq

Mi a típusrendszer használatával foglalkozunk.

Típusok:

length : String → Int         "hello" : String
----------------------------------------------
              length hello : Int

plus : Int × Int → Int        (2 , 3) : Int × Int
-------------------------------------------------
              plus (2 , 3) : Int

List : Type → Type

lengthInt    : List Int    → Int
lengthChar   : List Char   → Int
lengthString : List String → Int

length : (A : Type) → List A → Int

Haskellben megadható a négyzetes mátrixok típusa (de bonyolult)

Az alábbi típusok már nem:

  • fix-hosszú listák (tömbből ne lehessen kiindexelni)

  • rendezett listák

  • kiegyensúlyozott fák, AVL-fák, B-fák

  • 13 és 45 közötti számok

Agdában ezek is megadhatók.

Példa ugyanarra a programra, egyre kifinomultabb típusokkal:

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)

Tematika:

  • nulladrendű logika

  • elsőrendű logika

  • klasszikus logika

  • funkcionális programozás Agdában

  • induktív típusok

  • koinduktív típusok

Cél:

  • bizonyítottan helyes gyorsrendezés

Számonkérés:

  • beadandó kiírása minden héten óra után, két héttel később beadási határidő

  • vizsgán Agda programozás

Egyéb:

  • kísérleti fázis

  • kérdezzetek

Gyakorlati dolgok

Telepítés:

Emacs használat:

Feladatok:

Propozicionális logika

Ítéletváltozók: X, Y, Z.

Szabályok:

C állítás C létrehozása Egy p : C feltétel felhasználása
A → B λ a → ? p ?
tt
abort _ p
? , ? proj₁ p vagy proj₂ p
inj₁ ? vagy inj₂ ? case _ ? ? p
C p

A t : A jelölés azt jelenti, hogy a t bizonyítás bizonyítja az A állítást.

Bizonyítás létrehozása:

  1. Bemegyünk egy lyukba (ezeket ?-el vagy {!!}-el lehet lyukat létrehozni), ott C-c C-,-t nyomunk. Ezzel megtudjuk, hogy mi a cél (Goal:) és a vízszintes vonal (----) alatt ott vannak a feltételeink (amiket már tudunk a bizonyításhoz).

    C-c C-, helyett nyomhatunk C-u C-u C-c C-,-t, ekkor az összes rövidítést feloldaja az Agda, és úgy írja ki a célt és a feltételeket.

  2. Beírunk valamilyen bizonyítást, majd C-c C-.-ot nyomunk, ez kiírja, hogy amit beírtunk, az mit bizonyít (Have:).

    Lehet, hogy _123 és hasonló ún. metaváltozókat ír ki, ezek bármik lehetnek, tehát például _123 → _123 speciális esetei lehetnek X → X vagy Y → Y. _123 → _124 speciális esetei lehetne X → Y vagy Y → X stb.

    Hogyan adjuk meg a bizonyítást?

    1. Ha a cél ugyanaz, mint valamelyik feltétel, akkor egyszerűen megadjuk a feltételt (fenti táblázat utolsó sora).

    2. Ha a cél valamilyen logikai összekötős állítás, akkor azt fenti táblázatban a megfelelő létrehozó operátorral tudjuk létrehozni.

      Például, ha a cél X → Y, akkor λ x → ?-t írunk.

    3. Ha vannak feltételeink, azokból a fenti táblázatban megadott felhasználó operátorokkal tudunk újabb bizonyításokat létrehozni.

      Például, ha a cél Y, és van egy p : X → Y, akkor p ?-et írunk.

  3. Elfogadjuk, amit a lyukba írtunk: C-c C-space.

  4. Ha még van lyuk, akkor ugrás az 1. pontra.

Elsőrendű logika

Halmazok: M, N.

Predikátumok (unáris relációk, állítások az M halmaz elemeiről): P, Q. Tehát ha m egy M-beli elem, akkor P m és Q m állítások.

Bináris reláció M és N között: R. Tehát ha m egy M-beli elem, n pedig egy N-beli elem, akkor R m n egy állítás.

A t : A azt jelenti, hogy t az A állítás bizonyítása, és m : M azt jelenti, hogy m az M halmaz egy eleme. Azért ugyanaz a jelölés, mert Agdában ezek a fogalmak nincsenek megkülönböztetve.

A ∀x.P x-et ∀(x : M) → P x-el jelöljük (a szimbólum elhagyható). A ∃x.P x-et ∃ M λ x → P x-el jelöljük.

A fenti táblázatot kiegészítjük az univerzális () és az egzisztenciális () kvantorokkal.

C állítás C létrehozása Egy p : C feltétel felhasználása
A → B λ a → ? p ?
tt
abort _ p
? , ? proj₁ p vagy proj₂ p
inj₁ ? vagy inj₂ ? case _ ? ? p
C p
∀(x : M) → P x λ x → ? p ?
∃ M λ x → P x (? ,' ?) proj₁' p vagy proj₂' p

Függvények

Ha van M és N halmazunk, akkor M → N-el jelöljük az M értelmezési tartományú és N értékkészletű függvények halmazát. Függvényeket λ-val tudunk létrehozni és applikációval () tudunk felhasználni (hasonlóan az implikációhoz és univerzális kvantorhoz).

O halmaz O létrehozása Egy t : O elem felhasználása
M → N λ m → ? t ?

A függvényekre még a következő egyenlőségek is teljesülnek:

  • (λ x → t) u = t[x ↦ u] (tehát t, ahol az x összes előfordulását u-val helyettesítjük, ezt β-egyenlőségnek is nevezik)

  • λ x → (f x) = f (ezt η-egyenlőségnek is nevezik)

Peano számelmélet

Egy halmazunk van, , és egy relációnk, az egyenlőség .

Tehát bármely a : ℕ és b : ℕ számra a ≡ b egy állítás, azt fejezi ki, hogy a egyenlő b-vel. Ezt propozicionális egyenlőségnek nevezzük, és megkülönböztetjük a definíció szerinti egyenlőségtől, melyet a = szimbólummal jelölünk. egy reláció, utóbbi egy metaelméleti jelölés, mellyel rövidítéseket (definíciókat) vezetünk be.

Egyenlőséget létrehozni a következőképp tudunk bármely M halmazra.

    a : M
--------------
refl a : a ≡ a

Ha már van egy egyenlőségünk, a következőket tehetjük vele.

  p : a ≡ b      p : a ≡ b    q : b ≡ c
-------------    ----------------------
sym p : b ≡ a      trans p q : a ≡ c

a : M    b : M    p : a ≡ b    f : M → N
----------------------------------------
         cong f p : f a ≡ f b

elemeit a zero és a suc Peano-konstruktorokkal tudjuk létrehozni.

                  n : ℕ
--------        ---------
zero : ℕ        suc n : ℕ

Függvények természetes számokon:

z : M    s : M → M    n : ℕ
---------------------------
       Rec z s n : M

Rec z s zero = z
Rec z s (suc n) = s (Rec z s n)

Ha többparaméteres függvényt szeretnénk, iterálhatunk. Például az összeadás függvényt így írhatjuk: _+_ : ℕ → (ℕ → ℕ). Ez egy olyan függvény, melynek bemenete egy természetes szám, kimenete egy függvény, melynek bemenete egy természetes szám és kimenete is egy természetes szám.

Teljes indukció. Ha minden n természetes számra van egy P n állításunk (Pl. P n = zero + n ≡ n).

z : P zero    s : ∀(n : ℕ) → P n → P (suc n)    n : ℕ
-----------------------------------------------------
                   Ind P z s n : P n

Magasabbrendű logika

M : Set azt jelenti, hogy M egy halmaz.

A : Set azt jelenti, hogy A egy állítás.

P : M → Set azt jelenti, hogy P egy predikátum M-en, tehát minden m : M-re P m : Set (tehát P m állítás).

D : Set → Set azt jelenti, hogy minden A állításra D A egy állítás. Például:

  • Decidable : Set → Set, Decidable A azt jelenti, hogy A egy eldönthető állítás. Decidable = λ A → A ∨ ¬ A

E : Set → Set azt jelenti, hogy minden M halmazra E M egy állítás. Például:

  • Nonempty : Set → Set, Nonempy M azt jelenti, hogy az M halmaz nem üres. Nonempty = λ M → ∃ M λ x → ⊤.

A kizárt harmadik elve (LEM, law of excluded middle, tertium non datur) azt mondja, hogy minden állítás eldönthető.

Implicit paraméterek: {A : Set}{B : Set} → A → B → A ∧ B.

Set típusa Set₁. Set₁ : Set₂ stb.

Curry-Howard izomorfizmus

Az állításokat tekinthetem bizonyítások halmazainak. Az alábbi táblázat szemlélteti az összefüggést.

Állítás Halmaz
egyelemű halmaz
üres halmaz
A ∧ B A × B
A ∨ B A ⊎ B (diszjunkt unió)
A → B A → B
∃ A λ x → P x { x ∈ A, P x}
∀ A λ x → P x Π(x ∈ A).P x
a ≡ b a és b egyenlőségei

A halmazokon egyenlőségeink vannak, amik bizonyításokon nem voltak, például az alábbiak:

(λ x → t) u = t[x ↦ u]

proj₁ (t , u) = t
proj₂ (t , u) = u

case P f g (inj₁ a) = f a
case P f g (inj₂ b) = g b

Típuselmélet

A típuselméletben állítások illetve halmazok helyett típusokról beszélünk.

Egy típust az alábbi szabályokkal vezetünk be (néhány esetleg hiányozhat):

  • típuskonstruktorok (type formation)
  • konstruktorok (bevezetés, introduction)
  • eliminátorok (eliminator)
  • számítási szabályok (computation rules, β rules)
  • egyediségi szabályok (uniqueness rules, η rules)

A szabályokat lásd a tt.agda fájlban.