\documentclass[dvipsnames, hyperref={colorlinks=true,urlcolor=blue}]{beamer}

\usepackage[magyar]{babel}
\usepackage[mathletters]{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{amsmath}
\usepackage{amsfonts}

\usecolortheme{crane}

\newcommand{\comment}[1]{}

%include polycode.fmt

\begin{document}
\title{Dependent type-ok és az Agda}
\author{
  Dr. Érdi Gergő \\
  \url{http://gergo.erdi.hu/}}
\date{ELTE IK, 2009. november 10.}
\titlepage
\begin{code}
module AgdaEloadas where
\end{code}

\begin{frame}{Magasabb kind-ú típusok}

\emph{Haskell}: Típus függhet más típustól: pl.

\begin{spec}
data List τ = Nil | Cons τ (List τ)
\end{spec}

  Ez mit is jelent? A |List| valójában egy típuskonstrukciós művelet:
  ha adott egy |τ| típus, akkor ahhoz létezik egy |List τ| (algebrai)
  típus is, a megfelelő két konstruktorral. Vagyis a |List| típusról
  képez le típusra:

  \begin{spec}
List : ⋆ -> ⋆
  \end{spec}
  
  Ahol a |⋆| jelenti a "valamilyen típust".

  Lényeg: típusok és értékek világa egymástól teljesen el van választva.

  Ugyanez Agdában:

\begin{code}
data List (A : Set) : Set where
  nil :   List A
  cons :  A -> List A -> List A
\end{code}

\end{frame}

\begin{frame}{Dependent type-ok}

\emph{Agda}: Típus értéktől is függhet

Mit jelent ez? Például tegyük fel, hogy adott a természetes számok típusa:

\begin{code}
data Nat : Set where
  zero :  Nat
  succ :  Nat -> Nat
\end{code}

Ekkor értelmezhetjük egy adott |n|-re az |n| hosszú vektorok típusát:

\begin{code}
data Vec (A : Set) : Nat -> Set where
  nil   :   Vec A zero
  cons  : {n : Nat} -> A -> Vec A n -> Vec A (succ n)
\end{code}
\end{frame}

\section{Mire jó ez?}
\begin{frame}{Mire jó ez? Programhelyesség}

Vessük össze az alábbi két |map| változatot:

\begin{code}
map :  {A B : Set} ->
       (A -> B) -> List A -> List B
map f  nil          = nil
map f  (cons x xs)  = cons (f x) (map f xs)
{-""-}
vmap :  {A B : Set}{n : Nat} ->
        (A -> B) -> Vec A n -> Vec B n
vmap f  nil          = nil
vmap f  (cons x xs)  = cons (f x) (vmap f xs)
\end{code}

Abból, hogy ez típushelyes, következik, hogy tényleg ugyanolyan hosszú
vektort ad vissza, mint a bemenet:
\begin{spec}
vmap' :  {A B : Set}{n : Nat} ->
         (A -> B) -> Vec A n -> Vec B n
vmap' f _ = {-"\alert<2>{"-}nil{-"}"-} {-"\visible<2->{"-}-- Fordítási hibát ad!
{-"}"-}
\end{spec}

\end{frame}

\begin{frame}{Mire jó ez? Előfeltétel-ellenőrzés}

Értelmezhetjük egy adott |n|-re az |n|-nél kisebb természetes számok típusát:

\begin{code}
data FNat : Nat -> Set where
  zero  :  {n : Nat} -> FNat (succ n)
  succ  :  {n : Nat} -> FNat n -> FNat (succ n)
\end{code}

Ennek a segítségével le tudjuk írni a vektor-indexelés műveletét:

\begin{code}
_!!_ :  {A : Set}{n : Nat} -> Vec A n -> FNat n -> A
nil          !!  ()        -- |FNat zero| típusnak nincs eleme!
(cons x xs)  !!  zero      = x
(cons x xs)  !!  (succ m)  = xs !! m
\end{code}

\end{frame}

\section{Tételbizonyítás}
\begin{frame}{Tételbizonyítás}

Példa: Természetes számok összeadása kommutál.

\begin{displaymath}
\vdash \forall n, m \in \mathbb{N}: n+m = m + n
\end{displaymath}

Hogyan tudjuk a problémát megtámadni? Szedjük szét végtelensok
résztételre:

\begin{displaymath}
\left\{ n \in \mathbb{N}, m \in \mathbb{N} \right\} \vdash n+m = m + n
\end{displaymath}

Ha van egy konkrét $n$ és $m$, amiről annyit tudunk, amennyit a
baloldal állít, és ebből be tudjuk rájuk bizonyítani a jobboldalt,
akkor készen vagyunk.

\end{frame}

\begin{frame}{Tételbizonyítás: Reprezentáció}
%%Nyilván először definiálnunk kell az összeadást:

\begin{code}
_+_ : Nat -> Nat -> Nat
zero    +  m  = m
succ n  +  m  = succ (n + m)
\end{code}

A továbbiakban csakis erről az általunk definiált összeadásról tudunk
bármit is állítani és bizonyítani! (modellezés fontossága)

Az állításokból típusokat csinálunk:

\begin{code}
data Eq {A : Set} : A -> A -> Set where
  refl : {x : A} -> Eq x x
\end{code}

\end{frame}

\begin{frame}{Tételbizonyítás: Konstruktivitás}

Az előbbiek értelmében egy tételt akkor tudunk bebizonyítani, ha
minden konkrét esethez létre tudjuk az állítást hozni vagyis van egy
\emph{függvény}, ami általában elő tudja állítani az állítást, azaz
egy megfelelő elemét az állítást reprezentáló típusnak.

Vagyis az összeadás kommutativitásának tétele az, hogy létezik egy
olyan függvény, amelynek típusa:

\begin{spec}
thmPlusComm : (n m : Nat) -> Eq (n + m) (m + n)
\end{spec}

Indukció $\equiv$ rekurzió

\end{frame}
\begin{frame}{Tételbizonyítás $\equiv$ Bizonyításgenerálás}

Kezdjük el megírni a fenti függvényt

\begin{spec}
thmPlusComm zero      zero    = refl
thmPlusComm zero      (succ m)  = ??  -- |0 + m'   ==  m' + 0|
thmPlusComm (succ n)  zero      = ??  -- |n' + 0   ==  0 + n'|
thmPlusComm (succ n)  (succ m)  = ??  -- |n' + m'  ==  m' + n'|
\end{spec}

Ehhez szükségünk lesz az egyenlőség kongruencia-tulajdonságára és
tranzitivitására:

\footnotesize
\begin{code}
lemEqCong :  {A B : Set} {x y : A} (f : A -> B) ->
             Eq x y -> Eq (f x) (f y)
lemEqCong e refl = refl

{-""-}
lemEqTran :  {A B : Set} {x y z : A} ->
             Eq x y -> Eq y z -> Eq x z
lemEqTran refl refl = refl
\end{code}
\normalsize

\end{frame}

\begin{frame}{Tételbizonyítás: |thmPlusComm|}

\begin{code}
thmPlusComm : (n m : Nat) -> Eq (n + m) (m + n)
\end{code}

\begin{itemize}
\item
|0 + 0 == 0 + 0|: Mindkét oldal |0|-val egyenlő
\footnotesize
\begin{code}
thmPlusComm zero      zero      = refl
\end{code}
\normalsize

\item
|0 + m' == m' + 0|: Azonnal következik |0 + m == m + 0|-ból, mindkét
oldal rákövetkezőjét véve
\footnotesize
\begin{code}
thmPlusComm zero      (succ m)  = 
  lemEqCong succ (thmPlusComm  zero m)
\end{code}
\normalsize

\item
|n' + 0 == 0 + n'|: Hasonlóan
\footnotesize
\begin{code}
thmPlusComm (succ n)  zero      =
  lemEqCong succ (thmPlusComm n zero)
\end{code}
\normalsize
\end{itemize}
\end{frame}

\begin{frame}{Tételbizonyítás: |thmPlusComm| (folyt.)}
\begin{itemize}
\item |n' + m' == m' + n'|

Ez már keményebb dió, itt használjuk ki az egyenlőség tranzitivitását:
% TODO: sorszámozás
\footnotesize
\begin{align*}
n' + m'  & \equiv (n + m')'   \tag{1} \\
         & \equiv (m' + n)'   \tag{2} \\ 
         & \equiv ((m + n)')' \tag{3} \\
         & \equiv ((n + m)')' \tag{4} \\
         & \equiv (n' + m)'   \tag{3$'$} \\
         & \equiv (m + n')'   \tag{5} \\
         & \equiv m' + n'     \tag{1$'$} \qed
\end{align*}

\footnotesize
\begin{code}
thmPlusComm (succ n)  (succ m)  =
  lemEqCong succ                              -- (1)
    (lemEqTran {Nat} {Nat}
      (thmPlusComm n (succ m))                -- (2)
        (lemEqTran {Nat} {Nat}
          (lemEqCong succ                     -- (3)
            (thmPlusComm m n))                -- (4)
          (thmPlusComm (succ n) m)))          -- (5)
\end{code}
\normalsize
\end{itemize}
\end{frame}

\begin{frame}{Tételbizonyítás: Mit jelent a |thmPlusComm|?}

\begin{itemize}
\item Élő ember nem akarja meghívni ezt a függvényt
\item De a megléte bizonyítja azt, hogy az |(n m : Nat) -> Eq (n + m) (m + n)| típusnak van eleme!
\end{itemize}

Tehát a fenti típus olvasható úgy is, mint egy következtetés:
\begin{displaymath}
n, m \in \mathbb{N} \vdash n + m = m + n
\end{displaymath}

Hasonlóan a |lemEqCong| típusa: |{x y : A} (f : A -> B) -> Eq x y -> Eq (f x) (f y)|
nem jelent mást, mint
\begin{displaymath}
  x, y \in A, f \in A \rightarrow B \vdash (x = y) ⇒ (f(x) = f(y))
\end{displaymath}

Vagyis az Agda megvalósítja a \emph{Curry-Howard izomorfizmust}:
\begin{displaymath}
\text{Igaz állítás} \leftrightarrows \text{"Belakható" típus}
\end{displaymath}

\end{frame}

\begin{frame}{Tételbizonyítás: Helyesség és  teljesség}
\begin{itemize}

\item \emph{Helyesség}: Ha csak az Agda implementációban valamit nem
szúrtak el, akkor nem tudunk "hamis" típushoz elemet találni:
pl. nincs olyan kifejezés, aminek a típusa |(n : Nat) -> Eq n (succ n)|

Ehhez szükséges, hogy divergens kifejezéseket ne fogadjunk el, például
az alábbi Agda program hibás:

\begin{code}
nonsense : (n : Nat) -> Eq n (succ n)
nonsense n = {-"\alert<2->{"-}nonsense{-"}"-} n
\end{code}

\item \emph{Teljesség}: A fentiek alapján csak primitív rekurzív
kifejezéseket használhatunk! (különben a típusellenőrzéshez meg
kellene oldani a megállási problémát...) Például az
Ackermann-függvényt nem tudjuk definiálni:

\comment{
\begin{code}
{-# BUILTIN NATURAL Nat #-}
{-# BUILTIN ZERO    zero #-}
{-# BUILTIN SUC     succ #-}
\end{code}
}
\footnotesize
\begin{code}
Ack : Nat -> Nat -> Nat
Ack zero      x         = x + 1
Ack (succ i)  zero      = {-"\alert<3->{"-}Ack{-"}"-} i 1
Ack (succ i)  (succ x)  = {-"\alert<3->{"-}Ack{-"}"-} i ({-"\alert<3->{"-}Ack{-"}"-} (i + 1) x)
\end{code}
\normalsize
\end{itemize}
\end{frame}
\begin{frame}{(Ackermann-függvény másodrendű primitív rekurzív)}
\begin{code}
Ack' : Nat -> Nat -> Nat
Ack'  zero      = λ x -> x + 1
Ack'  (succ i)  = ack'
  where ack' : Nat -> Nat
        ack'  zero      = Ack' i 1
        ack'  (succ x)  = Ack' i (ack' x)
\end{code}
\end{frame}

\section{Programhelyesség}
\begin{frame}{Összefoglalva: Hogyan lesz ebből programhelyesség?}
\begin{itemize}

\item Ha ügyesek a típusaink, a függvényeink típusa jól leírja a
specifikációjukat (ld. |map| vs. |vmap|). Ha átmegy a típusellenőrzőn,
akkor megfelel a specifikációnak.

\item A függvényeink tulajdonságait tételként is megfogalmazhatjuk, és
az imént látott módon bizonyíthatjuk őket. Például ha adott az |id|
függvény:

\begin{code}
id : {A : Set} -> A -> A
id x = x
\end{code}

akkor ennek a lényeges tulajdonsága:

\begin{code}
thmIdId : {A : Set} {x : A} -> Eq x (id x)
thmIdId = refl
\end{code}

\end{itemize}
\end{frame}

\begin{frame}{Köszönöm a figyelmet}
További információ:
\begin{itemize}
\item \href{http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf}
{Ulf Norell: \emph{Dependently Typed Programming in Agda}}
\item \href{http://wiki.portal.chalmers.se/agda/}{\emph{Agda wiki}}
\item \href{http://www.cs.chalmers.se/Cs/Research/Logic/book/}
{Nordström, Petersson, Smith: \emph{Programming in Martin-Löf's Type Theory}}
\end{itemize}
\end{frame}

\section{Példa: Rendezett vektorok}
\begin{frame}{Példa}
Az alábbiakban egy nemtriviális tulajdonságot mutatok be: azt, hogy egy lista rendezett.
\end{frame}

%% Innentől az egyszerűbb olvahatóság kedvéért matematikai notációt használunk
%format (succ n) = n "^{\prime}"
%format (nil) = "[\ ]"
%format (cons x xs) = x "\mathop{:}" xs
%format _≤_ = "\cdot \le \cdot"
%format _∼_ = "\cdot ∼ \cdot"

\begin{frame}{Példa: Rendezés}

\footnotesize

%format _==_ = "\cdot \equiv \cdot"
\begin{code}
Rel : Set -> Set₁
Rel A = A -> A -> Set

data _==_ {A : Set} : Rel A where
  refl : {x : A} -> x == x

lem-cong :  forall {A B x y} (f : A -> B) ->
            x == y -> (f x) == (f y)
lem-cong p refl = refl
{-""-}
data Reflexive {A : Set} (_∼_ : Rel A) : Set where
  refl : ((x : A) -> x ∼ x) -> Reflexive _∼_

data Transitive {A : Set} (_∼_ : Rel A) : Set where
  tran : ({x y z : A} -> x ∼ y -> y ∼ z -> x ∼ z) -> Transitive _∼_

data Antisymmetric {A : Set} (_∼_ : Rel A) : Set where
  asym : ({x y : A} -> x ∼ y -> y ∼ x -> x == y) -> Antisymmetric _∼_
{-""-}  
data Ordering  {A : Set} (_≤_ : Rel A) : Set where
  ord :  Reflexive _≤_ -> Transitive _≤_ ->
         Antisymmetric _≤_ -> Ordering _≤_
\end{code}
\comment{
\begin{code}
{-""-}
data OrderedSet {A : Set} (_≤_ : Rel A) : Set where
  ordered : Ordering _≤_ -> OrderedSet _≤_
\end{code}
}
\end{frame}

\begin{frame}{Példa: $\mathbb{N}$ rendezése}
%format _≤Nat_ = "\cdot \le_{\mathbb{N}} \cdot"
%format ≤Nat = "\le_{\mathbb{N}}"
\begin{code}
data _≤Nat_ : Nat -> Nat -> Set where
  least  :  (n : Nat) -> zero ≤Nat n
  cong   :  {n m : Nat} -> n ≤Nat m -> (succ n) ≤Nat (succ m)
\end{code}
\comment{
\begin{code}
data Bool : Set where
  true : Bool
  false : Bool
  
_<_ : Nat -> Nat -> Bool
_        <  zero     = false
zero     <  succ n   = true
succ m   <  succ n  = m < n

\end{code}
}
\tiny
\begin{code}
thm-nat-≤-refl : Reflexive _≤Nat_
thm-nat-≤-refl = refl refl'
  where  refl' : (n : Nat) -> n ≤Nat n
         refl' zero = least zero
         refl' (succ y) = cong (refl' y)

thm-nat-≤-tran : Transitive _≤Nat_
thm-nat-≤-tran = tran tran'
  where  tran' : {x y z : Nat} → x ≤Nat y → y ≤Nat z -> x ≤Nat z
         tran'  {z = z}  (least _)  q         =  least z
         tran'           (cong p)   (cong q)  =  cong (tran' p q)

thm-nat-≤-asym : Antisymmetric _≤Nat_ 
thm-nat-≤-asym = asym asym'
   where  asym' : {x y : Nat} -> x ≤Nat y -> y ≤Nat x -> x == y
          asym'  (least .0)  (least .0)  =  refl
          asym'  (cong p)    (cong q)    =  lem-cong succ (asym' p q)
        
thm-nat-≤ : Ordering _≤Nat_
thm-nat-≤ = ord thm-nat-≤-refl thm-nat-≤-tran thm-nat-≤-asym
        
\end{code}
\normalsize
\end{frame}
\begin{frame}{Példa: Rendezett sorozatok}
\small
\begin{code}
data Sorted   {A : Set} {_≤_ :  A -> A -> Set} (ord : Ordering _≤_) :
              {n : Nat} -> Vec A n -> Set where
  trivial0  :  Sorted ord nil
  trivial1  :  (x : A) -> Sorted ord (cons x nil)
  inherit   :  {n : Nat} {x y : A} {ys : Vec A n}
               -> x ≤ y -> Sorted ord (cons y ys)
               -> Sorted ord (cons x (cons y ys))
\end{code}
\comment{
\begin{spec}
-- insert-sort : forall {A n} (_≤_ : A -> A -> Set) -> Vec A n -> Vec A n
insert : forall {n} -> Nat -> Vec Nat n -> Vec Nat (succ n)
insert  x  nil                      = cons x nil
insert  x  (cons y ys)  with x < y
insert  x  (cons y ys)  | true      = cons x (cons y ys)
insert  x  (cons y ys)  | false     = cons y (insert x ys)

insert-sort : forall {n} -> Vec Nat n -> Vec Nat n
insert-sort nil                   = nil
insert-sort (cons x ys)           = insert x ys



-- thm-insert-sort :  forall {A n _≤_} (o : Ordering _≤_) ->
--                    (xs : Vec A n) -> Sorted o (insert-sort _≤_ xs)
thm-insert-sort :  forall {n} -> (xs : Vec Nat n) -> Sorted thm-nat-≤ (insert-sort xs)
thm-insert-sort nil                   = trivial0
thm-insert-sort (cons x nil)          = trivial1 x
thm-insert-sort (cons x (cons y ys))  with x < y
thm-insert-sort (cons x (cons y ys))  | true with insert-sort (cons x (cons y ys))
thm-insert-sort (cons x (cons y ys))  | true | ss = {!ss!}

\end{spec}
}
\end{frame}

\end{document}