Einleitung

Programmierung im Studium bisher

Worin besteht jetzt der Fortschritt?

Formen der deklarativen Programmierung

Definition: Funktionale Programmierung

Softwaretechnische Vorteile

…der funktionalen Programmierung

Beispiel Spezifikation/Test

import Test.LeanCheck

append :: forall t . [t] -> [t] -> [t]
append [] y = y
append (h : t) y = h : (append t y)

associative f = 
   \ x y z -> f x (f y z) == f (f x y) z
commutative f = \ x y -> ...

test = check (associative (append @Bool))

Übung: Kommutativität (formulieren und testen)

Beispiel Verifikation

app :: forall t . [t] -> [t] -> [t]
app [] y = y
app (h : t) y = h : (app t y)

Lemma: app x (app y z) .=. app (app x y) z

Proof by induction on List x
  Case []
    To show: app [] (app y z) .=. app (app [] y) z
  Case h:t
    To show: app (h:t) (app y z) .=. app (app (h:t) y) z
    IH: app t (app y z) .=. app (app t y) z

CYP https://github.com/noschinl/cyp,

ist vereinfachte Version
von Isabelle https://isabelle.in.tum.de/

Beispiel Parallelisierung (Haskell)

-- Länge der Collatz-Folge
collatz :: Int -> Int
collatz x = if x <= 1 then 0
  else 1 + collatz (if even x then div x 2 else 3*x+1)
-- Summe der Längen
main :: IO ()
main = print $ sum
    $ map collatz [1 .. 10^7]

wird parallelisiert durch Strategie-Annotation:

import Control.Parallel.Strategies
...
main = print $ sum
  $ withStrategy (parListChunk (10^5) rseq)
  $ map collatz [1 .. 10^7]

Beispiel Parallelisierung (C#, PLINQ)

vgl. Introduction to PLINQ

https://msdn.microsoft.com/en-us/library/dd997425(v=vs.110).aspx

Softwaretechnische Vorteile

…der statischen Typisierung

The language in which you write profoundly affects the design of programs written in that language.

For example, in the OO world, many people use UML to sketch a design. In Haskell or ML, one writes type signatures instead. Much of the initial design phase of a functional program consists of writing type definitions.

Unlike UML, though, all this design is incorporated in the final product, and is machine-checked throughout.

Simon Peyton Jones, in: Masterminds of Programing, 2009;

http://shop.oreilly.com/product/9780596515171.do

Deklarative Programmierung in der Lehre

Beziehungen zu weiteren LV: Voraussetzungen

Anwendungen:

Konzepte und Sprachen

Funktionale Programmierung ist ein Konzept. Realisierungen:

Die Erkenntnisse sind sprachunabhängig.

Gliederung der Vorlesung

Anwendungen dieser Konzepte

Literatur (allgemein)

Literatur (speziell diese VL)

Alternative Quellen

Organisation der LV

Übungen KW 15 (vor Vorlesung)

Übungen

Aufgaben (allgemeines)

Aufgaben

SS 26: Aufgabe 1, 4, 5

  1. Digitale Selbstverteidigung

    1. Welche Daten gibt Ihr Browser preis?

      Starten Sie in einer Konsole den Befehl nc -l -p 9999

      (Konsole soll sichtbar bleiben)

      Rufen Sie im Browser die Adresse http://localhost:9999 auf, beobachten Sie die Ausgabe in der Konsole.

      Wie (personen)spezifisch ist diese Information?

    2. Wie können weitere Informationen extrahiert werden? Verwenden Sie https://www.eff.org/press/releases/test-your-online-privacy-protection-effs-panopticlick (Electronic Frontier Foundation, 2015–)

    3. Stellen Sie Firefox datenschutzgerecht ein. (Das beginnt mit der Default-Startseite!)

      Zeigen Sie die Benutzung von temporary containers, von Profilen (z.B. ein Profil für Browsing im Screen-Share).

      Führen Sie Browser-Plugins uMatrix, uBlockOrigin vor.

  2. zu: E. W. Dijkstra: Answers to Questions from Students of Software Engineering (Austin, 2000) (EWD 1035)

    • „putting the cart before the horse“

      • übersetzen Sie wörtlich ins Deutsche,

      • geben Sie eine entsprechende idiomatische Redewendung in Ihrer Muttersprache an,

      • wofür stehen cart und horse hier konkret?

  3. sind die empfohlenen exakten Techniken der Programmierung für große Systeme anwendbar?

    Erklären Sie „lengths of …grow not much more than linear with the lengths of …“.

    • Welche Längen werden hier verglichen?

    Modellieren Sie das System als Graph, die Knoten sind die Komponenten, die Kanten sind deren Beziehungen (direkte Abhängigkeiten).

    • Welches asymptotische Wachstum ist bei undisziplinierter Entwicklung des Systems zu befürchten?

    • Welche Graph-Eigenschaft impliziert den linearen Zusammenhang?

    • Wie gestaltet man den System-Entwurf, so daß diese Eigenschaft tatsächlich gilt? Welchen Nutzen hat das für Entwicklung und Wartung?

  4. Lesen Sie E. W. Dijkstra: On the foolishness of "natural language programming" https://www.cs.utexas.edu/users/EWD/transcriptions/EWD06xx/EWD667.html

    und beantworten Sie

    • womit wird “einfaches Programmieren” fälschlicherweise gleichgesetzt?

    • welche wesentliche Verbesserung brachten höhere Programmiersprachen, welche Eigenschaft der Maschinensprachen haben sie trotzdem noch?

    • warum sollte eine Schnittstelle narrow sein?

    • welche formalen Notationen von Vieta, Descartes, Leibniz, Boole sind gemeint? (jeweils: Wissenschaftsbereich, (heutige) Bezeichnung der Notation, Beispiele)

    • warum können Schüler heute das lernen, wozu früher nur Genies in der Lage waren?

    • Übersetzen Sie den Satz “the naturalness of …obvious”.

    Geben Sie dazu jeweils an:

    • die Meinung des Autors, belegt durch konkrete Textstelle und zunächst wörtliche, dann sinngemäße Übersetzung

    • Beispiele aus Ihrer Erfahrung

  5. Über ein Monoid \((M,\circ, 1)\) mit Elementen \(a, b\in M\) (sowie eventuell weiteren) ist bekannt: \(a^2= b^2 = (ab)^2 = 1\).

    Dabei ist \(ab\) eine Abkürzung für \(a\circ b\) und \(a^2\) für \(aa\), usw.

    • Geben Sie ein Modell mit \(1\neq a\neq b\neq 1\) an.

    • Überprüfen Sie \(ab = ba\) in Ihrem Modell.

    • Leiten Sie \(ab=ba\) aus den Monoid-Axiomen und gegebenen Gleichungen ab.

    Das ist eine Übung zur Wiederholung der Konzepte abstrakter und konkreter Datentyp sowie Spezifikation.

  6. im Rechnerpool live vorführen:

    • ein Terminal öffnen

    • ghci starten (in der aktuellen Version), Fakultät von 100 ausrechnen

    • Datei F.hs mit Texteditor anlegen und öffnen, Quelltext f = ... (Ausdruck mit Wert 100!) schreiben, diese Datei in ghci laden, f auswerten

    Dabei wg. Projektion an die Wand:

    Schrift 1. groß genug und 2. schwarz auf weiß.

    Vorher Bildschirm(hintergrund) aufräumen, so daß bei Projektion keine personenbezogenen Daten sichtbar werden. Beispiel: export PS1="$ " ändert den Shell-Prompt (versteckt den Benutzernamen).

    Vorführung der Aufgaben auf Pool-Rechner

Daten

Wiederholung: Terme

Beispiele: Signatur, Terme

Abmessungen von Termen

Induktion über Termaufbau (Beispiel)

Algebraische Datentypen (benannte Notation)

Algebraische Datentypen (positionelle Not.)

Datentyp mit mehreren Konstruktoren

Mehrsortige Signaturen

Bsp.: \(S=\{Z,B\}, \Sigma=\{0 \mapsto ([],Z), p \mapsto ([Z,Z],Z),\) \(e\mapsto ([Z,Z],B), a\mapsto([B,B],B)\}\).

Rekursive Datentypen

Daten mit Baum-Struktur

Übung Terme

Hausaufgaben

Allgemeine Hinweise zu Arbeit und Präsentation im Pool:

SS 26: 2, 4, 5

  1. (Pflicht-Aufgaben im autotool beachten.)

  2. Geben Sie einen Typ \(T\) (eine data-Deklaration) an, der alle Terme der einsortigen Signatur \(\Sigma=\{E/0, F/2, G/3\}\) enthält.

    Konstruieren Sie Elemente dieses Typs.

    Geben Sie \(t\in\operatorname{Term}(\Sigma)\) an mit

    • \(\operatorname{\textsf {height}}(t)=2\) und \(|t|\) möglichst klein

    • \(\operatorname{\textsf {height}}(t)=2\) und \(|t|\) möglichst groß

  3. Geben Sie einen Typ (eine data-Deklaration) mit genau 71 Elementen an. Sie können weitere Data-Deklarationen benutzen. Minimieren Sie die Gesamt-Anzahl der Konstruktoren. Bsp:

    data Bool = False | True ; data T = X Bool Bool

    dieser Typ T hat 4 Elemente, benutzt ingesamt 3 Konstruktoren (False,True,X)

  4. Beweisen Sie \(\forall \Sigma: \forall t\in\operatorname{Term}(\Sigma): \operatorname{\textsf {height}}(t) \le |t|-1\).

    durch Induktion über den Term-Aufbau.

    • Induktions-Anfang: \(t=f()\) (nullstelliges Symbol \(f\))

    • Induktions-Schritt:

      \(t=f(t_1,\dots,t_k)\) (\(k\)-stelliges Symbol \(f\), für \(k>0\))

      dabei Induktions-Voraussetzung: die Behauptung gilt für \(t_1,\ldots,t_k\).

      Induktions-Behauptung: …für \(t\).

    Für welche Terme \(t\) gilt Gleichheit? Wo sieht man das im Beweis?

  5. wieviele Elemente des Datentyps data T = L | B T T haben …

    • die Größe 9

    • die Größe \(\le 9\)

    • die Höhe \(0, 1, 2, 3\), Zusatz: größere konkrete Werte, allgemein (Formel)

    Sie müssen diese Elemente nicht alle einzeln angeben.

    Bestimmen sie ihre Anzahl durch dynamische Programmierung (von Hand).

Aufgaben autotool (Beispiele)

  1. einen Term in einer mehrsortigen Signatur angeben (Programmiersprache: Java)

    Gesucht ist ein Ausdruck vom Typ int
in der Signatur
    Foo e;
    String g;
    static char a ( Bar x, String y, String z );
    static Bar b ( Foo x );
    static int c ( int x, String y );
    static int d ( char x, Foo y, String z );
    static Foo f ( int x );
    static String h ( Foo x, String y, char z );

    Lösungsansatz: d (a (b (e), ...), ...)

  2. Fill holes (_) (replace with one item)
and ellipsis (...) (replace with several items)
in the following, so that the claim at the top becomes true.

For this exercise, each data declaration can only refer to types defined earlier -
not to itself or later (it cannot be recursive).

size_of (T) == 71 where 
  { data Bool =  False | True 
  ; data Col =  R | G | B 
  ; data S =  ... 
  ; data T =  ...  
  }

Programme

Plan

Bezeichnungen für Teilterme

dabei bezeichnen:

Operationen mit (Teil)Termen

Operationen auf Termen mit Variablen

Termersetzungssysteme

Termersetzungssysteme als Programme

dieses Berechnungsmodell ist im allgemeinen

Konstruktor-Systeme

Bsp: TRS \(R=\{(f(Z(),y),y),(f(S(x),y),S(f(x,y)))\}\)
über Signatur \(\Sigma=\{f/2,Z/0,S/1\}\)

nur Teilterme mit Wurzel \(f\) können ersetzt werden.

Für TRS \(R\) über Signatur \(\Sigma\): Symbol \(s\in\Sigma\) heißt

Das TRS \(R\) heißt Konstruktor-TRS, falls:

Beispiele: \(R_1=\{a(b(x)) \to b(a(x))\}\) über \(\Sigma_1=\{a/1,b/1\}\),

\(R_2=\{f(f(x,y),z) \to f(x,f(y,z))\) über \(\Sigma_2=\{f/2\}\)?

Funktionale Programme sind ähnlich zu Konstruktor-TRS.

Funktionale Programme (Bsp. und Vergleich)

Alternative Notation f. Gleichungssystem

Mehrfachverzweigung

data N = Z | S N ; data Bool = False | True
positive :: N -> Bool
positive x = case x of { Z -> False ; S x' -> True }

Eigenschaften von Muster-Mengen

eine Mustermenge (in einem case-Ausdruck, in einem Gleichungssystem) heißt

Bespiele (für data T = A | B T | F T T)

Sicheres Verarbeiten algebraischer Daten

…Verarbeiten algebraischer Daten vom Typ T:

Pattern Matching in versch. Sprachen

Rechnen mit Wahrheitswerten

Syntax für Unterprogramm-Aufrufe

Syntax für Fallunterscheidungen

Übung Term-Ersetzung

Für die Signatur \(\Sigma=\{f/1,g/3,c/0\}\):

Für die Signatur \(\Sigma=\{Z/0, S/1, f/2\}\):

Dabei wurde angewendet:

Abkürzung für Anwendung von 0-stelligen Symbolen: anstatt \(Z()\) schreibe \(Z\). (Vorsicht: dann kann man Variablen nicht mehr von 0-stelligen Symbolen unterscheiden. Man muß dann immer die Signatur explizit angeben oder auf andere Weise vereinbaren, wie man Variablen erkennt, z.B. „Buchstaben am Ende das Alphabetes (\(\dots,x,y,\dots\)) sind Variablen“, das ist aber riskant)

Übung Fallunterscheidungen

Für die Deklarationen

-- data Bool = False | True   (aus Prelude)
data T = F T | G T T T | C

entscheide/bestimme für jeden der folgenden Ausdrücke:

1. case False of { True -> C }
2. case False of { C -> True }
3. case False of { False -> F F }
4. case G (F C) C (F C) of { G x y z -> F z }
5. case F C of { F (F x) -> False }
6. case F C of { F x -> False ; True -> False }
7. case True of { False -> C ; True -> F C }
8. case True of { False -> C ; False -> F C }
9. case C of { G x y z -> False; F x -> False; C -> True }

GHC: Bibliotheken installieren und benutzen

Übung Programmierung

Hausaufgaben

SS 26: Aufgaben 1, 4, 5

  1. Arithmetik auf Peano-Zahlen

    • Für \(R=\{ f(S(x),y) \to f(x, S(y)), f(Z,y) \to y\}\)

      bestimme alle \(R\)-Normalformen von \(f(S(Z), S(Z))\).

    • für \(R_d = R\cup\{ d(x)\to f(x,x) \}\)

      bestimme alle \(R_d\)-Normalformen von \(d(d(S(Z)))\).

    • Bestimme die Signatur \(\Sigma_d\) von \(R_d\).

      Bestimme die Menge der Terme aus \(\operatorname{Term}(\Sigma_d)\), die \(R_d\)-Normalformen sind.

    • Welche Rechenoperationen simulieren die Regeln für \(f\), für \(d\)?

    • welche Terme haben große Normalformen?

  2. Simulation von Wort-Ersetzung durch Term-Ersetzung.

    Abkürzung für mehrfache Anwendung eines einstelligen Symbols: \(A(A(A(A(x)))) = A^4(x)\)

    • für \(\{ A(B(x)) \to B(A(x)) \}\)

      über Signatur \(\{A/1, B/1, E/0\}\):

      bestimme Normalform von \(A^k (B^k (E))\)

      für \(k=1, 2, 3,\) allgemein.

    • für \(\{ A(B(x)) \to B(B(A(x))) \}\)

      über Signatur \(\{A/1, B/1, E/0\}\):

      bestimme Normalform von \(A^k (B (E))\)

      für \(k=1, 2, 3,\) allgemein.

  3. für die Signatur \(\{A/2, D/0\}\):

    • definiere Terme \(t_0=D, t_{i+1} = A(t_i, D)\).

      Zeichne \(t_3\). Bestimme \(|t_i|,\operatorname{depth}(t_i)\) .

    • für \(S=\{ A(A(D,x),y)\to A(x,A(x,y)) \}\)

      bestimme \(S\)-Normalform(en), soweit existieren, der Terme \(t_0, t_1, \dots, t_4\).

      Geben Sie für \(t_2\) die ersten Ersetzungs-Schritte explizit an.

    • Normalform von \(t_i\) allgemein.

  4. Für die Deklarationen

    -- data Bool = False | True   (aus Prelude)
data S = A Bool | B | C S S

    entscheide/bestimme für jeden der folgenden Ausdrücke:

    • syntaktisch korrekt?

    • Resultat-Typ (statische Semantik)

    • Resultat-Wert (dynamische Semantik)

    • Menge der Muster ist: disjunkt? vollständig?

    1. case False of { True -> B }
2. case False of { B -> True }
3. case C B B of { A x -> x }
4. case A True of { A x -> False }

5. case A True of { A x -> False ; True -> False }
6. case True of { False -> A ; True -> A False }
7. case True of { False -> B ; False -> A False }
8. case B of { C x y -> False; A x -> x; B -> True }

    weitere Beispiele selbst herstellen und dann in der Übung die anderen Teilnehmer fragen.

  5. für selbst definierte Wahrheitswerte: deklarieren, implementieren und testen Sie:

    • die zweistellige Antivalenz,

    • die Implikation,

    • die dreistellige Majoritätsfunktion.

    import qualified Prelude
data Bool = False | True deriving Prelude.Show
not :: ...
xor :: ...
...

    Definieren Sie die Majorität auf verschiedene Weisen

    • mit einer Gleichung (evtl. mit case, evtl. geschachtelt)

    • ohne case (evtl. mehrere Gleichungen)

    • mit einer Gleichung ohne Fallunterscheidung, mittels anderer (selbst definierter) Funktionen

  6. für binäre Bäume ohne Schlüssel

    data Tree = Leaf | Branch Tree Tree

    deklarieren, implementieren und testen Sie ein einstelliges Prädikat über solchen Bäumen, das genau dann wahr ist, wenn das Argument eine ungerade Anzahl von Blättern enthält.

    Diese Anzahl nicht ausrechnen, sondern direkt den Wahrheitswert!

  7. in welchen Fällen zeigt der Compiler GHC(i) die Warnung overlapping patterns? https://downloads.haskell.org/ghc/latest/docs/users_guide/using-warnings.html#ghc-flag-Woverlapping-patterns

    Desgl. incomplete patterns?

    Definieren Sie formal. Vergleichen Sie mit Def. disjunkt und vollständig aus VL.

    Geben Sie Beispiele an mit selbst gebauten data-Typen.

    also nicht die Beispiele aus der Dokumentation - keine Maschinen- oder andere Zahlen (Int, Integer), keine polymorphen Container (Tupel, Listen).

  8. Der Haskell-Standard enthält

      data  Ordering    =  LT | EQ | GT

    Für diesen Typ gibt es eine Operation (<>), Bsp.

    ghci> LT <> GT    -- Resultat ist  LT

    • implementieren Sie diese Funktion (unter anderem Namen) durch eine möglichst kurze Fallunterscheidung. op x y = case x of ...

    • ist sie kommutativ? assoziativ?

    • besitzt die Operation ein linksneutrales Element? ein rechtsneutrales? eine Umkehr-Operation? (ist das Monoid eine Gruppe?)

    Testen Sie die Übereinstimmung der Definitionen sowie das Vorliegen der Eigenschaften mit leancheck, Bsp.

    ghci> import Test.LeanCheck
ghci> check $ \ (x :: Ordering) -> (x <> x) == x

    wie heißt die hier getestete Eigenschaft?

  9. (Nachtrag statische Semantik, TODO: das sollte auf eine separate Folie) Beantworten Sie durch den Haskell-Standard (Language Report):

    warum ist der folgende Ausdruck statisch falsch?

    -- data Bool = False | True   (aus Prelude)
data S = A Bool | B | C S S -- wie oben
case C B (C (A True) B) of { C x (C y x) -> True }

    Erläuterungen zur Fehlermeldung siehe https://errors.haskell.org/messages/GHC-10498/, aber Verweis auf Standard fehlt dort, selbst suchen unter https://haskell.org/documentation/.

    Welcher Abschnitt erklärt Fallunterscheidung? Dort wird Grammatik-Variable pat verwendet. In welchem anderen Abschnitt stehen deren Regeln? Nach diesen Regeln steht ein Satz, darin ein Begriff (ein Adjektiv) für eine Eigenschaft, die das Muster im Beispiel eben nicht hat.

    Für Term-Ersetzungs-Regeln ist es erlaubt, in der logischen Programmierung auch, in der funktionalen üblicherweise nicht, weil die Implementierung des pattern matching dann deutlich teurer wäre. Warum?

Aufgaben autotool (Beispiele)

  1. gesucht ist für das System
 TRS { variables = [ x, y, z ]
   , rules = 
     [ f ( f ( x, y ), z ) -> f ( x, f ( y, z ) )
     , f ( x, f ( y, z ) ) -> f ( f ( x, y ), z ) 
     ]   }
eine Folge von Schritten
von     f ( a, f ( f ( b, f ( c, d ) ), e ) )
nach    f ( f ( a, f ( b, c ) ), f ( d, e ) )

    Lösungs-Ansatz:

    ( f ( a, f ( f ( b, f ( c, d ) ), e ) )
, [ Step  { rule_number = 1  , position = [ ]
     , substitution = listToFM 
        [ (x, a), (z, e), (y, f (b, f (c, d))) ] 
     }                 ] )
  2. import Test.LeanCheck
import Test.LeanCheck.Extras

data T = A | B deriving (Show, Eq)

f :: T ->  T ->  T
f A A = A
f A B = B
f B A = B
f B B = A
-- ersetzen Sie die Lücke (_) durch eine oder mehrere geschachtelte Fallunterscheidungen
g :: T -> T -> T
g x y = _ 

instance Listable T where tiers = [[A,B]]

aufgabe1 = Prop "(f = g)" $ \ x y -> f x y == g x y

    • bearbeiten Sie das auf Ihrem eigenen Rechner (siehe Hinweise auf voriger Folie „GHC: Bibliotheken “),

      laden Sie das Resultat dann in autotool hoch.

    • jede Lücke _ ist zunächst ein statischer Fehler.

      Führen Sie in GHCi das Kommando :set -fdefer-typed-holes aus und laden das Modul neu (:r)
      (alternativ: so starten ghci -fdefer-typed-holes)

      Danach ist jede Lücke statisch korrekt,
      ergibt aber bei Auswertung einen Laufzeitfehler.

      Das erleichtert die schrittweise Programmierung.

      Vgl. Glasgow Haskell Compiler, 6.2.19. Typed Holes,

      https://downloads.haskell.org/ghc/latest/docs/users_guide/exts/typed_holes.html

Beweise

Motivation

Formale Beweise

CYP: Gleichungsketten

CYP: Fallunterscheidung

Peano-Zahlen

Spezifikation und Test

Bsp: Addition von Peano-Zahlen

Spezifikation und Verifikation

Beweis für: Addition von Peano-Zahlen ist assoziativ

Bezeichnungen in Beweisen durch Induktion

CYP: Induktion

Bsp. Programm-Konstruktion/Induktion

Induktion mit Generalisierung

Induktion über Bäume (IA)

Induktion über Bäume (IS)

Multiplikation von Peano-Zahlen

Minimum

Subtraktion

Hausaufgaben

SS 25: 1, 3, 4

  1. Für die Funktion

    f :: N -> N 
f Z = Z ; f (S x) = S (S (f x))

    beweisen Sie (erst auf Papier, dann mit CYP)

    f (plus x y) = plus (f x) (f y)

    durch Induktion nach x.

    Papier: Verwenden Sie die angegebenen Bezeichnungen für die Beweis-Schritte, geben Sie IA, IV, IB explizit an.

  2. Die übliche Peano-Addition ist

    plus Z y = y ; plus (S x) y = S (plus x y)

    Eine andere Implementierung der Addition (vgl. früher angegebenes Termersetzungssystem) ist

    plus' Z y = y ; plus' (S x) y = plus' x (S y)

    Beweisen Sie mit Cyp

    forall x :: N, y :: N : plus' x y .=. plus x y

    Beweisen Sie dazu als Hilfssatz

    forall x :: N, y :: N : plus x (S y) .=. plus (S x) y

    In dieser Induktion nach \(x\) müssen Sie das andere Argument \(y\) generalisieren, da es zwischen Induktionsvoraussetzung und Induktionsbehauptung unterschiedlich ist.

  3. Implementieren Sie Peano-Multiplikation und -Potenz.

    Formulieren, testen (leancheck) und beweisen (Papier, CYP) Sie einige Eigenschaften.

    CYP: formulieren Sie ggf. Hilfssätze als Axiome, d.h., ohne Beweis—aber mit Tests.

  4. Für zweistelliges min (siehe Folie) und max auf \(\NN\):

    1. Geben Sie eine äquivalente vollständige Spezifikation an, die keine Fallunterscheidung benutzt, sondern nur Addition.

    2. Implementieren Sie min und max nur durch Addition und Subtraktion (\(\ominus\)).

    3. testen (optional: und beweisen) Sie, daß Ihre Implementierung die Spezifikation erfüllt

    4. Implementieren Sie nur mit min und max:

      • den Median von drei Argumenten

      • (optional) den Median von fünf Argumenten

      Geben Sie Tests an (optional: Beweis)

  5. für das TRS \(R=\{A(A(D,x),y)\to A(x,A(x,y))\}\) über der Signatur \(\Sigma=\{D/0,A/2\}\), vgl. frühere Aufgabe,

    1. die Menge (Folge) aller \(R\)-Normalformen ist \(N_0=D, N_1=A(D,N_0), \dots, N_{k+1}=A(D,N_k),\dots\).

      warum gibt es keine anderen \(R\)-Normalformen?

    2. Die \(R\)-Normalform von \(A(N_l,N_r)\) ist \(N_k\) mit \(k=2^l+r\).

      1. Geben Sie Beispiele an (auf Papier oder maschinell)

      2. beweisen Sie durch vollständige Induktion nach \(l\).

        (Auf Papier, aber mit korrekten Bezeichnungen.)

      3. welches sind die Terme (z.B.: der Größe 11) mit größter Normalform?

Aufgabe Autotool (Beispiel)

a :: T -> T
b :: T -> T
axiom E : forall x :: T : a(b(a(x))) .=. x
Lemma :
  forall x :: T : a(b(b(b(a(a(x)))))) .=. b(b(a(x)))
Proof by rewriting         a(b(b(b(a(a(x))))))
    (by E) .=. _
    (by E) .=. _
    ...
           .=. b(b(a(x)))
QED

Das ist ein Modell für schnittstellen-orientierte Programmierung. Der abstrakte Datentyp \(T\) besteht aus Signatur (\(\{a/1, b/1\}\)) und Axiom \(E\), es ist nichts bekannt über tatsächliche Implementierung.

Plan (vorläufig)