Organisatorisches

Ablauf Lehrveranstaltung und Prüfung

Quellen

Übungen KW 15 (vor Vorlesung)

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]->[Bool]->[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

Aufgaben (allgemeines)

Aufgaben

SS 24: Aufgabe 1

  1. Digitale Selbstverteidigung

    1. Welche Daten gibt Ihr Browser preis?

      Starten Sie in einer Konsole den Befehl ncat --listen --source-port 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. Ü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.

  5. 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).

    Wer eigenen Rechner im Pool benutzt:

    • Aufgaben wie oben und

    • ssh-Login auf einen Rechner des Pools

      (damit wird die Ausrede GHC (usw.) geht auf meinem Rechner nicht hinfällig)

    • ssh-Login oder remote-Desktop-Zugriff von einem Rechner des Pools auf Ihren Rechner (damit das projiziert werden kann, ohne den Beamer umzustöpseln)

    (falls das alles zu umständlich ist, dann eben doch einen Pool-Rechner benutzen)

  6. welcher Typ ist zu erwarten für die Funktion,

    • (wurde bereits in der Übung behandlelt) die das Spiegelbild einer Zeichenkette berechnet?

    • die die Liste aller (durch Leerzeichen getrennten) Wörter einer Zeichenkette berechnet?

      f "foo bar" = [ "foo", "bar" ]

    Suchen Sie nach Funktionen dieses Typs mit https://www.haskell.org/hoogle/, erklären Sie einige der Resultate, welches davon ist das passende, rufen Sie diese Funktion auf (in ghci).

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

SS 24: Aufgaben 2, 3, 4.

  1. autotool-Aufgabe 15-2

    Allgemeine Hinweise zur Bearbeitung von Haskell-Lückentext-Aufgaben in autotool:

    • Schreiben Sie den angezeigten Quelltext (vollständig! ohne zusätzliche Leerzeichen am Zeilenanfang!) in eine Datei mit Endung .hs, starten Sie ghci mit diesem Dateinamen als Argument

    • ändern Sie den Quelltext: ersetzen Sie undefined durch einen geeigneten Ausdruck, hier z.B.

      solution = S.fromList [ False, G ]

      im Editor speichern, in ghci neu laden (:r)

    • reparieren Sie Typfehler, werten Sie geeignete Terme aus, hier z.B. S.size solution

    • werten Sie test aus, wenn test den Wert True ergibt, dann tragen Sie die Lösung in autotool ein.

  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ß

    Allgemeine Hinweise zu Arbeit und Präsentation im Pool:

    • beachten Sie https://www.imn.htwk-leipzig.de/~waldmann/etc/pool/ (PATH und ggf. LD_LIBRARY_PATH)

    • Freigabe (für Dozenten-Rechner) mit krfb, Einmalpaßwort

    • Schrift schwarz auf weiß! Vernünftige Schriftgröße (Control-Plus)!! Gleichzeitig sichtbar (d. h.: keine Verdeckungen, Umschaltungen): Aufgabenstellung, Programmtext, Ausgabe/Fehlermeldungen. Wenn der Desktop-Hintergrund sichtbar ist—wurde Platz verschenkt!!!

  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

    dieses T hat 4 Elemente, 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, \dots, k, \dots\)

    Sie müssen diese Elemente nicht alle einzeln angeben.

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

Aufgaben autotool

  1. Ersetzen Sie undefined, so daß der Ausdruck test den Wert True hat.

    module Blueprint where
import qualified Data.Set as S
-- aus Prelude importiert:
-- data Bool = False | True
data C = R | G | B deriving (Eq, Ord, Show)
data T = X C Bool | Y Bool | Z deriving (Eq, Ord, Show)
solution :: S.Set T
solution = S.fromList undefined
test :: Bool
test = S.size solution == 9

    Ansatz einer Lösung:

    solution = S.fromList [ X R False, Y True ]

  2. 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), ...), ...)

Programme

Plan

Bezeichnungen für Teilterme

dabei bezeichnen:

Operationen mit (Teil)Termen

Operationen mit Variablen in Termen

Termersetzungssysteme

Termersetzungssysteme als Programme

dieses Berechnungsmodell ist im allgemeinen

Konstruktor-Systeme

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

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

Übung: diese Eigenschaft formal spezifizieren

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\}\):

definierte Symbole? Konstruktoren? Konstruktor-System?

Funktionale Programme sind ähnlich zu Konstruktor-TRS.

Funktionale Programme (Bsp. und Vergleich)

Alternative Notation f. Gleichungssystem

Pattern Matching

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

Eigenschaften von Case-Ausdrücken

ein case-Ausdruck heißt

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

data und case

typisches Vorgehen beim 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 Pattern Matching, Programme

Hausaufgaben

SS 24: 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?

    • Zusatz: Geben Sie eine Funktion \(c:\NN\to\NN\) an, für die gilt: \(\forall n\in\NN: \forall t,t'\in\operatorname{Term}(\Sigma_d): |t|\le n\wedge t\to_{R_d}^* t' \Rightarrow |t'|\le c(n)\).

  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!

Aufgaben autotool

  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))) ] 
     }                 ] )

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 24: Aufgaben 2, 4 von hier sowie Aufgabe 4 aus Abschnitt Daten (\(\forall \Sigma:\forall t\in\operatorname{Term}(\Sigma):\operatorname{\textsf {height}}(t)\le |t|-1)\))

  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.

Polymorphie

Definition, Motivation

Beispiele f. Typkonstruktoren (I)

Beispiele f. Typkonstruktoren (II)

Anwendung von Maybe

Polymorphe Funktionen

Bezeichnungen f. Polymorphie

data List e = Nil | Cons e (List e)

Operationen auf Listen (I)

data List a = Nil | Cons a (List a)

Von der Spezifikation zur Implementierung

Operationen auf Listen (II)

Operationen auf Bäumen

data List e = Nil | Cons e (List e)
data Bin e = Leaf | Branch (Bin e) e (Bin e)

Knotenreihenfolgen

Adressierug von Knoten (False \(=\) links, True \(=\) rechts)

Statische Typisierung und Polymorphie

Bsp. für Programm ohne statischen Typ

Nutzen der stat. Typisierung und Polymorphie

Konstruktion von Objekten eines Typs

Aufgabe (Bsp): x :: Either (Maybe ()) (Pair Bool ())

Lösung (Bsp):

Insgesamt x = Right y = Right (Pair False ())

Vorgehen (allgemein)

Bestimmung des Typs eines Bezeichners

Aufgabe (Bsp.) bestimme Typ von x (erstes Arg. von get):

at :: List N -> Tree a -> Maybe a
at p t = case t of
  Node f ts -> case p of
    Nil -> Just f
    Cons x p' -> case get x ts of
      Nothing -> Nothing
      Just t' -> at p' t'

Lösung:

Vorgehen zur Typbestimmung eines Namens:

Übung Polymorphie

Hausaufgaben

SS 24: für KW 19: 1, 2, 5; für KW 20 (Zusatz) 3, 6, 7.

  1. für die folgenden Datentypen: geben Sie einige Elemente an (ghci), geben Sie die Anzahl aller Elemente an.

    1. Maybe (Maybe Bool)

    2. Either (Bool, ()) (Maybe ())

    3. Foo (Maybe (Foo Bool)) mit data Foo a = C a | D

    stellen Sie (dann in der Übung) ähnliche Aufgaben

    geben Sie ein möglichst kleines Programm an, das nur aus data-Deklarationen besteht, und das einen Typ mit 100 (Zusatz: 1000) Elementen definiert.

    Diskussion: vergleiche frühere Aufgabe. Ein solcher Typ ist

    Maybe (Maybe (Maybe .... (Maybe ()) .. ))

    mit insgesamt nur drei Konstruktoren (Nothing, Just, ()).

    Also sollte man zur gerechten Messung der Programmgröße die Anzahl der Konstruktoren und die Größe der Typ-Ausdrücke addieren.

  2. Implementieren Sie die Post-Order Durchquerung von Binärbäumen.

    (Zusatz: Level-Order. Das ist schwieriger.)

    Verwenden Sie nur die in der VL definierten Typen (data List a = ..., nicht Prelude.[])

    und Programmbausteine (case _ of)

    Geben Sie einen Algorithmus zur Lösung der Rekonstruktions-Aufgabe (preorder, postorder) an.

  3. Beweisen Sie (auf Papier, Zusatz: mit Cyp)

    forall xs . reverse (reverse xs) == xs

    Verwenden Sie ggf.

    rev (app xs ys) = app (rev ys) (rev xs)

    oder andere Hilfssätze ohne Beweis (aber mit Beispielen und Tests)

  4. (zu voriger Woche, Typ ist nicht polymorph)

    Definitionen ergänzen; Eigenschaften testen (Einzelfälle, Leancheck), beweisen (Papier oder Cyp)

    data Tree = Leaf | Branch Tree Tree
size :: Tree -> N
leaves :: Tree -> N
branches :: Tree -> N
odd :: N -> Bool
Lemma : 
  size t .=. plus (leaves t) (branches t)
Lemma : odd (size t)

    Folien Induktion über Bäume benutzen.

  5. zum Typ Optional<T> aus JDK (im Vergleich zu Maybe t aus Haskell)

    • mit jshell (23-ea) im Pool vorführen:

      mit of ein Objekt konstruieren, darauf isPresent anwenden

    • geben Sie den Typ von isPresent in Haskell an, Hinweis: :: Maybe t -> _,

      benutzen Sie https://hoogle.haskell.org/ zur Suche nach Funktionen mit diesem Typ (geben Sie den Typ der Funktion ein, nicht den (vermuteten) Namen)

      Rufen Sie solche Funktionen auf (ggf. das passende Modul importieren. Keine neuen Bibliotheken installieren, base genügt)

    • geben Sie den Haskell-Typ von orElse (aus JDK) an. Implementieren Sie diese Funktion in Haskell.

  6. für diese Deklarationen (die Konstruktor-Namen sind abgekürzt, P(air), L(eaf), B(ranch), damit man in Beispielen nicht so viel tippen muß)

    data Pair a b = P a b
data Tree k = L k | B (Tree (Pair k k))

    ergänzen Sie den Ausdruck B (B (L _)) :: Tree Bool

    Welche Form haben die Elemente von Tree k allgemein? Geben Sie weitere Beispiel an.

    Bemerkung: Dieser Typkonstruktor Tree heißt nicht regulär, denn er ist rekursiv und bei Rekursion wird das Typ-Argument geändert. Zum Vergleich: data List t = Nil | Cons t (List t) ist regulär, denn das Argument von List bleibt t.

  7. Darstellung von Zahlen als binäre Bäume:

    import Numeric.Natural
data T = Z | F T T
value :: T -> Natural
value Z = 0
value (F x y) = 2 ^ value x + value y
-- Beispiel:
value (F (F (F Z Z) (F Z Z)) (F Z Z)) = 9

    • geben Sie Terme mit Werten \(0, 1, 2, 3, 4, 14, 144\) an (falls möglich, jeweils mehrere)

    • begründen Sie, daß jede natürliche Zahl durch T darstellbar ist

    • ein Baum t :: T heißt vernünftig, wenn t == Z oder t = F x y und 2 ^ value x > value y und x und y beide vernünftig sind.

      begründen Sie, daß jede natürliche Zahl genau eine vernünftige Darstellung besitzt.

    • Implementieren Sie für vernünftige Bäume:

      Vergleiche (eq :: T -> T -> Bool, gt :: T -> T -> Bool), Nachfolger (s :: T -> T), Addition (p :: T -> T -> T)

      Hinweis: mit gen :: Natural -> T (als Umkehrfunktion von value) geht das so: p x y = gen (value x + value y). Gesucht sind Lösungen ohne Umweg über Natural.

      Ansatz: Klar ist s Z = F Z Z. Wann ist s (F x y) = F x (s y) falsch? Wie kann man das 1. feststellen, 2. reparieren?

Lambda-Kalkül: Syntax und dynamische Semantik (Auswertung)

Funktionen als Daten

Der Lambda-Kalkül

Freie und gebundene Variablen(vorkommen)

Semantik des Lambda-Kalküls: Reduktion \(\to_\beta\)

Relation \(\to_\beta\) auf \(\Lambda\) (ein Reduktionsschritt)

Es gilt \(t \to_\beta t'\), falls

Ein (Teil-)Ausdruck der Form \((\lambda x.B)A\) heißt Redex.
(Dort kann weitergerechnet werden.)

Ein Term ohne Redex heißt Normalform.
(Normalformen sind Resultate von Rechnungen.)

Umbenennung von lokalen Variablen

Falsches Binden lokaler Variablen

Semantik …: gebundene Umbenennung \(\to_\alpha\)

Lambda-Terme: verkürzte Notation

Ein- und mehrstellige Funktionen

Lambda-Ausdrücke in C#

Lambda-Ausdrücke in Java

Lambda-Ausdrücke in Javascript

$ node

> let f = function (x){return x+3;}
undefined

> f(4)
7

> ((x) => (y) => x+y) (3) (4)
7

> ((f) => (x) => f(f(x))) ((x) => x+1) (0)
2

Ein AST für Lambda-Terme

Hausaufgaben

SS 24: 6, (3 oder 4 oder 5); Zusatz: 1 (diese), 7 (vorige Woche) (Nachfolger und Plus für Zahlen als Binärbäume)

  1. bvar und fvar implementieren, Testfälle vorführen (aus Skript und weitere)

  2. pos, get und put implementieren, Testfälle vorführen.

  3. für \(t=\lambda f x . f (f x)\): AST von \(t t S Z\) zeichnen,

    Normalform bestimmen: 1. auf Papier, 2. mit ghci (dabei \(Z\) und \(S\) als Konstruktoren der Peano-Zahlen)

    3. mit JS (node), dabei \(Z=0\) und \(S=(x=>x+1)\).

  4. für \(s=\lambda x y z . x z(y z)\) und \(k=\lambda a b.a\):

    Auswertung von \(s k k 0\) in Haskell, in Javascript (node),

    optional: in C# (csharp), Java (jshell), oder anderer Sprache

  5. Für \(n\in\NN\) bezeichnet (nur für diese Aufgabe, die eckigen Klammern bedeuten oft etwas anderes) \([n]\) den Lambda-Ausdruck \(\lambda f x. f^n(x)\),

    dabei ist \(f^n(x)\) die \(n\)-fach iterierte Anwendung von \(f\) auf \(x\),

    also \([0]=\lambda f x.x, [1]=\lambda f x. f x, [2]=\lambda f x.f (f x), [3]=\lambda f x.f (f (f x))\) usw.

    die Normalform von \([2] s z\) ist \(s (s z)\), das entspricht der Peano-Repräsentation der Zahl 2.

    • für \(p=\lambda a b f x.a f (b f x)\): bestimmen Sie die Normalform von \(p [2] [1] s z\)

    • bestimmen Sie die Normalform von \([3] [2] s z\)

  6. zur Folie Falsches Binden lokaler Variablen (wurde in VL durch anderes Beispiel ersetzt):

    • abstrakte Syntax des Ausdrucks zeichnen (unter der Annahme eines zusätzlichen zweistelligen Symbols für Addition),

    • die Variablen-Bedingung für angegebenen Redex überprüfen,

    • lokale Umbenennung durchführen,

    • dann reduzieren bis Normalform (unter der Annahme einer zusätzlichen arithmetischen Regel für Addition)

L-K.: statische Semantik (Typisierung)

Motivation, Plan

Grundlagen zur Typisierung

Einfache (monomorphe) Typen

Verkürzte Notation für Typen

Typ-Abstraktion und -Applikation

Polymorphie: Notation

Polymorphie: Notation: Abkürzungen

Nützliche Funktionen höherer Ordnung

Der allgemeinste Typ eines Ausdrucks

Beispiel für Typ-Bestimmung

Aufgabe: bestimme den allgemeinsten Typ von \(\lambda f x. f(f x)\)

Stelligkeit von Funktionen

Beispiele Fkt. höherer Ord.

Fkt. höherer Ord. für Folgen

Fkt. höherer Ord. für Mengen

Polymorphe Unterprogr. in anderen Sprachen

Zusammenfassung, Ausblick

Übung

Hausaufgaben

SS 24: 1, 3, 5.

  1. für die Lambda-Ausdrücke

    1. \(\lambda f g h x y . f (g x) (h y)\):

    2. \((\lambda x.x x) (\lambda y.y y)\)

    3. \(\lambda x y z . x y (y z)\)

    4. \(\lambda a b . b (\lambda x . x a)\)

    AST zeichnen, allgemeinsten Typ bestimmen, falls möglich

    (1. von Hand, mit Begründung, 2. mit ghci überprüfen)

  2. für die Ausdrücke

    flip
flip flip
flip flip flip
...

    jeweils Argumente \(a_1 a_2\dots\) angeben (passende Anzahl), so daß der Wert von flip flip ... flip a1 a2 ... gleich True ist.

    Dabei alle Typargumente für alle flip explizit angeben.

  3. in Haskell: Lambda-Ausdrücke mit diesen Typen angeben, falls möglich:

    a -> (a -> c) -> c
a -> b
(a -> b) -> (b -> c) -> a -> c
a -> (a -> a) -> a
(a -> b) -> (a -> c) -> (b -> c -> d) -> a -> d

    mit ghci überprüfen (Typen anzeigen lassen)

    die Ausdrücke dann auch mit passenden Argumenten aufrufen, so daß der Wert True ist (oder von einem andern data-Typ, jedenfalls keine Funktion)

  4. (einige der) Funktionen compose, flip, curry, uncurry

    in C# (csharp) und Java (jshell) deklarieren (vorher prüfen, ob es die schon gibt) (anhand von Primärquellen)

    und aufrufen (dabei Typ-Argumente explizit angeben)

    Den Typ für 2-Tupel aus der jeweiligen Standardbibliothek benutzen.

  5. für Data.List, Data.Sequence

    die Funktionen partition, span, inits, tails

    1. aufrufen (in ghci Beispiele vorführen), dabei anwenden auf eine Liste/Folge von Bool

    2. die API-Dokumentation aufsuchen (https://hackage.haskell.org/)

    3. einige der dort angegebenen Eigenschaften als Leancheck-Property überprüfen, Beispiel:

      $ ghci -package containers -package leancheck
ghci> import qualified Data.Sequence as Q
ghci> import Test.LeanCheck
ghci> check $ \ (xs :: [Bool]) -> Q.reverse (Q.fromList xs) == Q.fromList (reverse xs)

      (vgl. ähnliche Aufgabe im autotool)

  6. Typisierung von \(s k k \textsf{False}\) (vgl. Aufgabe vorige Woche) in Java oder C#.

    Vorübung: in Haskell, dabei für \(s\) und \(k\) alle Typen deklarieren und alle Typ-Argumente angeben.

    i :: a -> a ; i = \ x -> x  -- nur für Beispiel
k :: a -> b -> a ; k = \ x y -> x
s :: (a -> b -> c) -> ... ; s = \ x y z -> x z (y z)

i @(Bool -> Bool) (i @Bool) False   -- Beispiel
s @(...) (k @...) (k @...) False

    in Java und C#: besteht Unterschied zwischen Werten und Methoden: Methoden können polymorph sein, Werte nicht.

    Lambda-Ausdrücke sind Werte, also nicht polymorph:

    Function<Boolean,Boolean> i = (x) -> x  // monomorph

    im Bespiel \(s k k \textsf{False}\) muß \(k\) polymorph sein, da es mit zwei verschiedenen Belegungen der Typ-Argumente benutzt wird.

    Lösung (d.h., Umweg): eine polymorphe nullstellige Methode schreiben, die den Lambda-Ausdruck liefert.

    $ jshell
jshell> class C {
  static <A> Function<A,A> i() { return (x)->x; }
  // hier s und k ähnlich deklarieren
}
jshell> C.<Function<Boolean,Boolean>>i().apply(C.<Boolean>i()).apply(false)

    In C# genauso, aber das apply entfällt.

    $ csharp
csharp> class C { public static Func<A,A> i<A>() { return x=>x; }} 
csharp> C.i<Func<Boolean,Boolean>>()(C.i<Boolean>())(false)

Aufgaben autotool (Beispiele)

  1. Gesucht ist eine Ableitung mit genau 4 Reduce-Schritten , die

        (\ z -> (\ u -> u z) (\ u v -> z)) ((\ z -> x y) x)

    überführt in

        (\ u v -> x y) (x y)

    Anfang einer Lösung:

    Aktueller Term ist
    (\ z -> (\ u -> u z) (\ u v -> z)) ((\ z -> x y) x)

Aktueller Schritt ist
    Step 
      { position = [ 1 ]
      , action = Reduce { formal = z, body = x y, argument = x } 
      }

Teilterm an Position 
[ 1 ] ist

    (\ z -> x y) x

Resultat der Anwendung auf den Teilterm ist
    x y

Ergebnis der Ableitung ist
    (\ z -> (\ u -> u z) (\ u v -> z)) (x y)

  2. Lückentext (undefined ersetzen)

    {-# language TypeApplications #-}

module Blueprint where

import Prelude hiding (takeWhile, dropWhile)
import Test.LeanCheck
import Test.LeanCheck.Function

data List a = Nil | Cons a (List a)
  deriving (Eq, Show)

instance Listable a => Listable (List a) where
  tiers = cons0 Nil \/ cons2 Cons

takeWhile :: (a -> Bool) -> List a -> List a
takeWhile p xs = case xs of
  Nil -> Nil
  Cons x xs' -> case p x of
    False -> Nil
    True -> Cons x (takeWhile p xs')

dropWhile :: (a -> Bool) -> List a -> List a
dropWhile p xs = case xs of
  Nil -> Nil
  Cons x xs' -> case p x of
    False -> undefined
    True -> undefined

append :: List a -> List a -> List a
append Nil ys = ys
append (Cons x xs') ys = Cons x (append xs' ys)

prop :: Eq a => (a -> Bool) -> List a -> Bool
prop  = \ p xs -> append (takeWhile p xs) (dropWhile p xs) == xs

test = holds 200 (prop @Bool)

-- Gegenbeispiele sichtbar mit:  checkFor 200 (prop @Bool)

Rekursionsmuster

Rekursion über Bäume (Beispiele)

Rekursion über Bäume (Schema)

f :: Tree a -> b
f t = case t of
  Leaf -> ...
  Branch l k r -> ... (f l) k (f r)

dieses Schema ist eine Funktion höherer Ordnung:

fold :: ( ... ) -> ( ... ) -> (Tree a -> b)
fold leaf branch = \ t -> case t of
  Leaf -> leaf
  Branch l k r -> 
     branch (fold leaf branch l) 
            k (fold leaf branch r)
summe = fold Z (\ x y z-> plus x (plus y z))

(bei Aufruf ist dann x=summe l, y=k, z=summe r)

Rekursion über Listen (Bsp. und Schema)

and :: List Bool -> Bool
and xs = case xs of 
  Nil -> True ; Cons x xs' -> x && and xs'
length :: List a -> N
length xs = case xs of
  Nil -> Z ; Cons x xs' ->  S (length xs')

fold :: b -> ( a -> b -> b ) -> List a -> b
fold nil cons xs = case xs of
    Nil -> nil
    Cons x xs' -> cons x ( fold nil cons xs' )
and = fold True (&&) 
length = fold Z ( \ x y ->  S y)

Rekursionsmuster (Prinzip)

Rekursionsmuster (Merksätze)

aus dem Prinzip ein Rekursionsmuster anwenden \(=\) jeden Konstruktor durch eine passende Funktion ersetzen folgt:

Argumente für Rekursionsmuster finden

systematisches experimentelles Vorgehen zur Lösung von:

Schreiben Sie Funktion \(f:T \to R\) als fold

Beispiel: reverse :: List a -> List a

Hausaufgaben

SS 24: 1, 3, wenn Zeit ist: 2, aber nur ist gerade.

  1. Wenden Sie die Vorschrift zur Konstruktion des Rekursionsmusters an auf die Typen

    Bool, Maybe a, Pair a b, Either a b

  2. implementieren Sie mit dem Rekursionsmuster auf Peano-Zahlen:

    • g :: N -> Bool mit \(g x=\) (\(x\) ist eine gerade Zahl)

    • plus, mal, hoch

  3. für den Datentyp der binären Bäume mit Schlüsseln nur in den Blättern

    data Tree a
  = Leaf a | Branch (Tree a) (Tree a)

    1. aus dem Typ das Rekursionsschema ableiten

        fold :: ...

    2. Beispiele (jeweils zunächst den Typ angeben!)

      • Anzahl der Blätter

      • Anzahl der Verzweigungsknoten

      • Summe der Schlüssel

      • die Tiefe des Baumes

      • der größte Schlüssel

      • der Schlüssel links unten (auf Position \(p \in 0^*\))

Aufgabe autotool (Beispiel)

Implementieren Sie tails mit fold:

{-# language TypeApplications #-}

module Blueprint where
import Test.LeanCheck
import Prelude hiding (head, map)

data List a = Nil | Cons a (List a) deriving (Eq, Show)

instance Listable a => Listable (List a) where
  tiers = cons0 Nil \/ cons2 Cons

fold :: r -> (a -> r -> r) -> List a -> r
fold nil cons xs = case xs of
  Nil -> nil
  Cons x xs' -> cons x (fold nil cons xs')

tails :: List a -> List (List a)
tails =
  fold undefined ( \ x y -> Cons undefined undefined )

prop :: Eq a => List a -> Bool
prop = \ xs -> head (tails xs) == xs

head :: List a -> a
-- partielle Funktion!
head (Cons x xs) = x

test :: Bool
test = and
  [ tails (Cons 1 (Cons 2 Nil))
    == Cons (Cons 1 (Cons 2 Nil)) (Cons (Cons 2 Nil) (Cons Nil Nil))
  , holds 100 (prop @Bool)
  ]

Rekursionsmuster (Forts.)

Rekursionsschema f. mehrstellige Fkt.

Rekursionsm. (Peano-Zahlen) (einst.)

Rekursionsm. (Peano-Zahlen) (zweist.) (I)

Rekursionsm. (Peano-Zahlen) (zweist.) (II)

Nicht durch Rekursionmuster darstellbare Fkt.

Darstellung mit Fold und Projektion

Zusammenfassung Rekursionmuster

Spezialfälle des Fold

Rekursion über Listen aus Std.-Bib.

das vordefinierte Rekursionsschema über Listen ist:

foldr :: (a -> b -> b) -> b -> ([a] -> b)
length = foldr ( \ x y -> 1 + y ) 0 -- Bsp

Aufgaben:

Weitere Übungsaufgaben zu Fold

Übung Rekursionsmuster

Implementierungen für natürlichen Zahlen

Merksätze

Hausaufgaben

SS 24: 1, 2, optional 6

  1. Beweisen Sie, daß die modifizierte Vorgängerfunktion

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

    kein fold ist.

    ggf. ergänzende Aufgaben in autotool (nicht vorführen):

    • Diese Funktion pre kann jedoch als Projektion einer geeigneten Hilfsfunktion h :: N -> (N,N) realisiert werden. Spezifizieren Sie h und geben Sie eine Darstellung von h als fold an.

    • Implementieren Sie die (modifizierte) Subtraktion minus mit fold (über das erste Argument) (und pre)

  2. für Listen aus Standardbibliothek:

    1. die Funktion scanr an Beispiele vorführen,

    2. mit foldr implementieren. Ansatz:

      scanr f s = foldr (\ x (y:ys) -> _ ) [s]

    3. die Funktion tails mit scanr implementieren

  3. Rekursionsmuster auf Eigenbau-Listen:

    • mit fold und ohne Rekursion implementieren:

      isPrefixOf :: Eq a => List a -> List a -> Bool

      siehe Folie Rekursionsmuster für mehrstellige Funktion, fold über das erste Argument. Ansatz:

      isPrefixOf = fold (\ ys -> True) (\ x p ys -> case ys of
  Nil -> _ ; Cons y ys' -> _)

      (Das Typ-Constraint Eq a bedeutet, daß der Operator (==) :: a -> a -> Bool benutzt werden kann, genaue Erklärung dazu später.)

    • die Eigenschaft isPrefixOf xs (append xs ys) mit Leancheck überprüfen (für xs :: List Bool)

      Diese Eigenschaft abändern und Gegenbeispiele diskutieren.

    • für isSuffixOf: 1. konkrete Testfälle, 2. allgemeine Eigenschaft, 3. Implementierung ohne Rekursion, ohne Fold, aber unter Benutzung von reverse angeben.

  4. Rekursionsmuster auf binären Bäumen (Schlüssel in Verzweigungsknoten)

    • Beweisen Sie, daß is_search_tree :: Tree N -> Bool kein fold ist.

    • diese Funktion kann jedoch als Projektion einer Hilfsfunktion h :: Tree N -> (Bool, Maybe (N,N)) erhalten werden, die für Bäume mit nicht-leerer Schlüsselmenge auch noch deren kleinstes und größtes Element bestimmt. Stellen Sie h als fold dar.

    Bemerkung zu \(\NN\) beachten. Hier ist Numeric.Natural sinnvoll.

  5. für binäre Bäume mit Schlüsseln in den Blättern:

    die strukturerhaltende Abbildung definieren

    mapt :: (a -> b) -> Tree a -> Tree b

    (1) durch direkte Rekursion, (2) durch fold

    die Aussage mapt id = id überprüfen (3) an konkreten Testfällen, (4) mit leancheck. Dazu

    instance Listable a => Listable (Tree a) where
  tiers = cons1 Leaf \/ cons2 Branch

  6. für binäre Bäume mit Schlüsseln in den Blättern: eine Funktion

    unfold :: (r -> Either k (r, r)) -> r -> Tree k

    definieren, so daß

    unfold (\ x -> if x == 0 then Left () else Right (x-1,x-1)) h

    einen vollständigen Binärbaum der Höhe \(h\) erzeugt.

    (+) in jedem Blatt soll die Höhe des gesamten Baumes stehen.

    (++) die Schlüssel in den Blättern sollen (von links nach rechts) \([0,1,2 \dots]\) sein

    Wie hoch ist, wieviele Blätter hat, wie heißt dieser Baum?

    unfold (\ x -> if x > 1 then Left () else Right (x-1,x-2)) h

    Ergänzen Sie die Beziehung zwischen fold und unfold: für alle g, l, b mit passenden Typen gilt:

    wenn  forall x : case g x of
                    Left k      -> l k == x
                    Right (y,z) -> _
dann  forall x : fold l b (unfold g x) == x

Eingeschränkte Polymorphie

Abstrakte Datentypen: Motivation

Abstrakte Datentypen: Beispiel

sortBy :: (a -> a -> Ordering) -> [a] -> [a]
sortBy ( \ x y -> ... ) [False, True, False]

Kann mit Typklassen so formuliert werden:

class Ord a where compare :: a -> a -> Ordering
sort :: Ord a => [a] -> [a]
instance Ord Bool where compare x y = ...
sort [False, True, False]

Typklassen in Bibliotheks-Schnittstellen

Unterschiede Typklasse/Interface (Anwend.)

Unterschiede Typklasse/Interface (Implem.)

Eingeschränkte generische Instanzen (I)

Eingeschränkte generische Instanzen (II)

class Show a where  show ::  a -> String -- Typklasse
-- eine konkrete Instanz
instance Show Bool where
  show False = "False" ; show True = "True"
-- eingeschränkte generische Instanzen:
instance Show a => Show [a] where
  show xs = brackets $ concat
          $ intersperse "," $ map show xs
instance (Show a, Show b) => Show (a,b) where ...
-- Anwendung:
show ([True,False],True) = "([True,False],True)"

Wörterbuch für instance Show ([Bool],Bool)

wird vom Compiler konstruiert aus der konkreten Inst. durch Anwendung der generischen Inst.-Regeln

Zusatz: Superklassen

Zusatz: Default-Implementierungen

Zusatz: (Eingeschränkt) polymorphe Literale

Benutzung von Typklassen bei Leancheck

Test.LeanCheck—Beispiel

Testen für beliebige Stelligkeit

Überblick über Leancheck-Implementierung

Typklassen/Interfaces: Vergleich, Ausblick

Hausaufgaben

SS 24: (1 oder 2), 5, optional: 4, 6

  1. diese Aufgabe für selbst definierten Datentyp T, mit Typklassen Eq und Ord aus der Standardbibliothek:

    Definieren Sie für data T = T Bool Bool Bool

    • instance Eq T als komponentenweise Gleichheit

    • instance Ord T als lexikografisches Produkt der Standard-Ordnung auf Bool (zitieren Sie zunächst die mathematische Definition, z.B. aus der VL Modellierung)

    Formulieren Sie allgemein (d.h., polymorph) als leancheck-Eigenschaft, daß die Relation (<=)

    • transitiv

    • antisymmetrisch

    ist und prüfen Sie das für Integer und für T.

    instance Listable T where tiers = cons3 T

leq_is_transitiv :: Ord a => a -> a -> a -> Bool
leq_is_transitiv = \ x y z -> _

check (leq_is_transitiv @T)

  2. diese Aufgabe für selbst definierten Datentyp T, mit Typklassen Semigroup und Monoid aus der Standardbibliothek:

    Definieren Sie für data T = T Bool Bool Bool

    • instance Semigroup T als komponentenweise Konjunktion

    • instance Monoid T als dazu passendes neutrales Element

    Formulieren Sie die Monoid-Axiome allgemein (d.h., polymorph) als Eigenschaft in Leancheck und überprüfen Sie diese für T.

    Geben Sie eine andere korrekte Monoid-Struktur für T an, die nicht kommutativ ist. Testen Sie diese Eigenschaft (leancheck soll das Gegenbeispiel finden).

  3. für Peano-Zahlen: deklarieren Sie instance Num N und implementieren Sie dafür (nur) (+) und (*)

    (mit den bekannten Definitionen als fold)

    Test: S (S Z) * S (S (S Z))

    und: S (S (S Z)) ^ 3 (warum funktioniert das?)

    Implementieren Sie fromInteger

    (rekursiv, mit if x > 0 then ... else ...)

    Test (polymorphes Literal) 42 :: N

  4. Modul Data.Map aus containers, Modul Data.HashMap aus unordered-containers:

    • warum hat fromList ein Typconstraint (oder sogar zwei) für den Schlüsseltyp k, aber nicht für den Werttyp a?

    • Erläutern Sie Typconstraints (oder deren Fehlen) für singleton

    für Data.Map:

    • warum haben die Typen von unionWith und intersectionWith unterschiedliche Anzahl von Typvariablen?

    • Erläutern Sie Typconstraints (oder deren Fehlen) für singleton, fromAscList, fromDistinctAscList

    • Definieren Sie einen Typ data K = ... deriving Eq. Implementieren Sie instance Ord K so, daß die Relation (<=) keine totale Ordnung ist.

      Zeigen Sie durch Beispiele, daß dann M.Map K v nicht funktioniert. Z.B.: mit M.insert eingefügter Schlüssel nicht in M.toList zu sehen, sichtbarer Schlüssel nicht gefunden mit M.lookup.

  5. für instance Semigroup Ordering, instance Monoid Ordering aus der Standardbibliothek:

    Bestimmen Sie die Wertetabelle von (<>).

    Überprüfen Sie (mit leancheck) die Axiome von Semigroup und Monoid. Ist die Verknüpfung kommutativ?

    Für den Datentyp data Pair a b = Pair a b: implementieren Sie den lexikografischen Vergleich

    instance (Ord a, Ord b) => Ord (Pair a b) where
  compare (Pair px py) (Pair qx qy) = _

    • mit Fallunterscheidungen

    • ohne Fallunterscheidung, aber mit (<>)

  6. Im Haskell-Standard (wo genau?) steht

    class  (Eq a) => Ord a  where  
    compare              :: a -> a -> Ordering  
    (<), (<=), (>=), (>) :: a -> a -> Bool  

    compare x y =
      if x == y then EQ else
      if x <= y then LT  else GT
 
    x <= y  = compare x y /= GT  
    x <  y  = compare x y == LT  
    x >= y  = compare x y /= LT  
    x >  y  = compare x y == GT

    1. nach den Deklaratioen

      data T = A | B deriving Eq
instance Ord T where
  { B <= A = False ; _ <= _ = True }

      Beschreiben Sie die Auswertung von A > B (Schritt für Schritt bis zum Resultat: welche Gleichungen werden benutzt?)

    2. nach den Deklarationen

      data S = C | D deriving Eq
instance Ord S -- keine Implementierung!

      beschreiben und begründen Sie die Rechnungen für

      • C < C

      • C < D

Objektorientierte Entwurfsmuster

Was und warum?

Was ist und wie wirkt Objektorientierung

Entwurfsmuster: Definition, Geschichte

Beispiel Strategie-Muster

Java: Funktionale Schnittstellen

Kompositum: Motivation

Kompositum: Beispiel

import javax.swing.*; import java.awt.*;
public class Composite  {
  public static void main(String[] args) {
    JFrame f = new JFrame ("Composite");
    f.setDefaultCloseOperation(JFrame.EXIT_ON_CLOSE);
    Container c = new JPanel (new BorderLayout());
    c.add (new JButton ("foo"), BorderLayout.CENTER);
    c.add (new JButton ("bar"), BorderLayout.SOUTH);
    Container d = new JPanel (new GridLayout (0,2));
    d.add (c); d.add (new JButton ("baz"));
    f.getContentPane().add(d);
    f.pack(); f.setVisible(true);      } }

Ziel ist eine Baumstruktur, leider imperativ konstruiert

(Konstruktor new JPanel(List<Component> cs) fehlt)

Kompositum: Definition

(Vorsicht: Begriff und Abkürzung nicht verwechseln mit abstrakter Datentyp \(=\) ein Typ, dessen Datenkonstruktoren wir nicht sehen)

Binäre Bäume als Komposita

Kompositum-Vermeidung

Kompositum und Visitor

Prüfungsmodus in autotool

Überblick, Verschiedenes

Verzögerte (bedarfsgesteuerte) Auswertung

Motivation: Datenströme

Folge von Daten:

aus softwaretechnischen Gründen diese drei Aspekte im Programmtext trennen,

aus Effizienzgründen in der Ausführung verschränken (bedarfsgesteuerte Transformation/Erzeugung)

Bedarfs-Auswertung, Beispiele

Beispiel Bedarfsauswertung

data Stream a = Cons a (Stream a)
nats :: Stream N ; nf :: N -> Stream N
nats = nf 0 ; nf n = Cons n (nf (n+1))
head (Cons x xs) = x ; tail (Cons x xs) = xs

Obwohl nats unendlich ist, kann Wert von head (tail (tail nats)) bestimmt werden:

   = head (tail (tail (nf 0)))
   = head (tail (tail (Cons 0 (nf 1))))
   = head (tail (nf 1))
   = head (tail (Cons 1 (nf 2)))
   = head (nf 2) = head (Cons 2 (nf 3)) = 2

es wird immer ein äußerer Redex reduziert

(Bsp: nf 3 ist ein innerer Redex)

Strictness

zu jedem Typ \(T\) betrachte \(T_\bot=\{\bot\}\cup T\)

dabei ist \(\bot\) ein Nicht-Resultat vom Typ \(T\)

Def.: Funktion \(f\) heißt strikt, wenn \(f(\bot)=\bot\).

Fkt. \(f\) mit \(n\) Arg. heißt strikt in \(i\),

falls \(\forall x_1 \dots x_n: (x_i=\bot) \Rightarrow f(x_1,\ldots,x_n)=\bot\)

verzögerte Auswertung eines Arguments
\(\Rightarrow\) Funktion ist dort nicht strikt

einfachste Beispiele in Haskell:

Beispiele Striktheit

Implementierung der verzögerten Auswertung

Begriffe:

bei jedem Konstruktor- und Funktionsaufruf:

Bedarfsauswertung in Scala

Diskussion

Anwendg. Lazy Eval.: Ablaufsteuerung

Anwendg. Lazy Eval.: Abstraktion der Programmablaufsteuerung, Modularität

Anwendg. Lazy Eval.: Streams

Primzahlen

primes :: [ Nat ]
primes = sieve ( from 2 )

from :: Nat -> [ Nat ]
from n = n : from ( n+1 )

sieve :: [ Nat ] -> [ Nat ]
sieve (x : ys) = 
  x : sieve (filter (\y ->0 < mod y x) ys)

(Das ist (sinngemäß) das Code-Beispiel auf https://www.haskell.org/)

Semantik von let-Bindungen

Beispiel für Lazy Semantik in Let

Übungsaufgaben zu Striktheit

Hausaufgaben

SS 24: 1, 6; optional: 2, 7, 8

  1. Aufgabe: strikt in welchen Argumenten?

    f x y z = case y || x of
  False -> y
  True -> case z && y  of
    False -> z
    True  -> False

    die Eigenschaft lt. Definition: (a) erklären und (b) mit ghci experimentell überprüfen

    Bereiten Sie eine ähnliche Aufgabe vor, die Sie in der Übung den anderen Teilnehmern stellen.

  2. Bestimmen Sie jeweils die ersten Elemente dieser Folgen (1. auf Papier durch Umformen, 2. mit ghci).

    Vorher für die Hilfsfunktionen (map, zipWith, concat):
    1. Typ feststellen, 2. Testfälle für endliche Listen

    1. f = 0 : 1 : f
    2. n = 0 : map (\ x -> 1 + x) n
    3. xs = 1 : map (\ x -> 2 * x) xs
    4. ys = False 
 : tail (concat (map (\y -> [y,not y]) ys))
    5. zs = 0 : 1 : zipWith (+) zs (tail zs)

    siehe auch https://www.imn.htwk-leipzig.de/~waldmann/etc/stream/

  3. Für Peano-Zahlen und Eigenbau-Listen implementieren:

    len :: List a -> N als fold,

    Vergleich (gt: greater than, größer als) wie folgt:

    gt :: N -> N -> Bool
gt Z y = _
gt (S x) Z = _
gt (S x) (S y) = gt _ _

    und diese Auswertung erklären:

    gt (len (Cons () (Cons () undefined)))
   (len (Cons () Nil))

    Unterschiede erklären zu

    length (() : () : undefined) > length (() : undefined)

  4. Folie Ablaufsteuerung: Ifthenelse (wenn) als Funktion in Haskell, in Javascript, Simulation der nicht-strikten Auswertung.

  5. Algorithmus aus Appendix A aus Chris Okasaki: Breadth-First Numbering: Lessons from a Small Exercise in Algorithm Design (ICFP 2000) implementieren (von where auf let umschreiben), testen und erklären

  6. für Peano-Zahlen mit plus, mal, hoch wie üblich (rekursiv oder mit fold) sowie gt wie vorige Aufgabe:

    wie teuer ist gt (hoch (S (S Z)) (hoch ...)) Z?

    gilt Monotonie der arithmetischen Funktionen?

    Bsp: folgt aus gt x y = True, daß gt (mal x (S Z)) (mal y (S Z)) = True? daß gt (mal (S Z) x) (mal (S Z) y) = True?

    Betrachten Sie Beispiele wie x = (S (S undefined)); y = (S Z).

  7. Def: \(f :: \texttt{Tree k}\to b\) heißt strikt in der Struktur, wenn für für alle \(t\) gilt: wenn \(t\) ein \(\bot\) an Stelle eines Konstruktors enthält, dann \(f (t) =\bot\).

    Entspr.: strikt in den Schlüsseln, wenn …\(\bot\) an Stelle eines Schlüssels….

    Bsp: nodes ist nicht strikt in den Schlüsseln, denn nodes (Branch Leaf undefined Leaf) = 3

    Untersuchen Sie diese Eigenschaften für die Funktionen aus früherer Aufgabe für Fold auf binären Bäumen.

  8. aus aktuellem Anlaß: Lazy Evaluation und Künstliche Intelligenz (Kapitel 5 aus Hughes 1984, vereinfacht:)

    Funktionen min und max für Peano-Zahlen implementieren, die in der Struktur möglichst lazy sind, Bsp: min (S Z) (S (S undefined)) = S Z

    Diese Funktionen verwenden für die minimax-Bewertung eines (Spiel)baums (binär, Schlüssel in den Blättern).

    Begründen Sie: diese Bewertung ist nicht strikt in der Struktur, d.h., der exakte Spielwert kann bestimmt werden, ohne alle Teilbäume anzusehen. (Hinweis: ein Bsp. ist im Paper)

    Vereinfach: Bewertung durch Bool (gewonnen/verloren). Was sind dafür min und max? Wie strikt sind diese?

Aufgabe autotool (Beispiel)

  1. Aufgabenstellung:

    For this set of declarations
{ g x y = case (f x y True x) of 
   { False -> f True True False x; True -> y }
; f z y p q = case p of { False -> True
   ; True -> case q of
     { False -> True; True -> False } } }
Prove that function g is not strict:
Write a call where at least one argument is  undefined,
such that the result is defined
(it has a head normal form with a constructor on top)
and will be obtained after at most 40 steps.

    Beispiel-Lösung: g True undefined

  2. Aufgabenstellung:

    Find a replacement expression for the hole (_) in the program
  { f z x = 
      case (g x (g x z)) of 
        { False -> False; True -> False }
  ; g z x = _ 
  }
such that evaluations of the following expressions
to head normal form gives these results:
  [ ( f undefined False, Defined )
  , ( f undefined True, Bottom )     ]

    Beispiel-Lösung:

    case z of {False -> False; True -> x}

    Beispiel-Bewertung (Ausschnitt)

    evaluate f undefined False
(must have result Defined)
    ** Address 0 allocate new Thunk (f undefined False) (listToFM [ ])
    >> compute head normal form for Address 0
        value at address is 
          Thunk (f undefined False) (listToFM [ ])
        ** clock tick 1
        is thunk, reduce it
        is application
        ** Address 1 allocate new Thunk undefined (listToFM [ ])
        ** Address 2 allocate new Thunk False (listToFM [ ])
        defining equations for function f 
          [ [ z, x ] -> case (g x (g x z)) of { False -> False; True -> False } ]
        >> find first applicable equation, return rhs and matching substitution
            ** clock tick 2
            >> multi_match [ z, x ]
            [ Address 1, Address 2 ]
                >> match z
                Address 1
                << match z
                Address 1
                result: Just (listToFM [ ( z, Address 1 ) ])
                >> match x
                Address 2
                << match x
                Address 2
                result: Just (listToFM [ ( x, Address 2 ) ])
            << multi_match [ z, x ]
            [ Address 1, Address 2 ]
            result: Just (listToFM [ ( x, Address 2 ), ( z, Address 1 ) ])
...

Fkt. höherer Ord. für Streams

Motivation

Motivation: Parallel-Verarbeitung

geeignete Fkt. höherer Ordnung \(\Rightarrow\) triviale Parallelisierung:

Func<int,int> f = x => ... // teure Rechnung
var s = Enumerable.Range(1, 20000)
     .Select( f ).Sum() ;
var s = Enumerable.Range(1, 20000)
     .AsParallel()
     .Select( f ).Sum() ;

Dadurch werden

vgl.

https://learn.microsoft.com/en-us/dotnet/standard/parallel-programming/introduction-to-plinq

Strom-Operationen

Strom-Produktion

Struktur-erhaltende Strom-Transf.

Zusatz: Struktur-erhaltende Abb. allgemein

Zusatz: Forderungen an Funktoren

Struktur-ändernde Strom-Transf.

Linq (Language integrated query) in C#

Kombination von Strömen mit SelectMany

Zusatz: Anwendung von Bind

Zusatz: do-Notation

Fold-Left: Beispiel

Fold-Left: Implementierung

Fold-Left: allgemeiner Typ

Zusammenfassung: Ströme

Hausaufgaben

SS 24: 1, 2, 8 oder 9; vorige Woche: 7, 8

  1. die Funktion fromBits :: [Bool] -> Integer, Beispiel fromBits [True,False,False,True,False]=18

    …als foldr oder als foldl ?

    Geben Sie die eine Darstellung an, begründen Sie, daß die andere unmöglich ist.

  2. Vervollständigen Sie die Gleichung

    foldl f a (map g xs) = foldl _ _ xs

    so, daß rechts kein map steht. Dieses Verschwinden des map heißt Fusion.

    Fusion mit foldr vgl. Gill, Launchbury, Peyton Jones: A Short Cut to Deforestation, FCPA 1993; https://dl.acm.org/doi/10.1145/165180.165214

    Vervollständigen Sie die Gleichung

    foldr f a xs = foldl _ _  (reverse xs)

    und testen Sie mit Leancheck. Verwenden Sie dabei Test.LeanCheck.Function, um auch f zu generieren.

  3. In einem Kommentar in GHC.List

    https://hackage.haskell.org/package/base-4.15.0.0/docs/src/GHC-List.html#filter

    stellt SLPJ (wer ist das?) fest, daß man in der Gleichung

    filter p (filter q xs) 
  = filter (\ x -> q x && p x) xs

    , die zur Programmtransformation während der Kompilation verwendet wird, die Reihenfolge der Argumente im Teilausdruck q x && p x nicht vertauschen darf. Warum—die Konjunktion ist kommutativ?

  4. Geben Sie jeweils die strukturerhaltende Transformation als Funktor-Instanz an:

    1. Binärbäume mit Schlüssel in Verzweigungsknoten

      data Tree a = ... 
instance Functor Tree where
  fmap f t = case t of ...
    2. data T a = T (Bool -> a)
instance Functor T where   fmap f (T g) = ...

    Überprüfen Sie (mit Leancheck) die Funktor-Axiome.

    Vergleichen Sie das Verhalten Ihrer Implementierung mit der von deriving Functor.

  5. warum ist keine der folgenden Instanzen korrekt? Überprüfen Sie statische Korrektheit (Typisierung) und dynamische Korrektheit (Axiome)

    1. instance Functor Maybe where fmap f m = m
    2. instance Functor Maybe where fmap f m = Nothing
    3. instance Functor [] where
  fmap f xs = reverse (map f xs)
    4. instance Functor [] where
  fmap f xs = take 1 (map f xs)

    bei (c) und (d) ist [] der Typkonstruktor für Listen aus der Standardbibliothek, map die korrekte Implementierung.

  6. (Funktionen aus Data.List)

    • implementieren Sie scanr mittels foldr.

      scanr f z = foldr (\x (y:ys) -> _) _

    • implementieren Sie scanr mittels mapAccumR.

      scanr f z = uncurry (:) . mapAccumR _ _

    • ergänzen Sie die allgemeingültige Aussage

      scanr f z (reverse xs) = _ (scanl _ _ xs)

  7. definieren Sie den Operator (>=>) durch

    f >=> g = \ xs -> f xs >>= g

    Ergänzen Sie, so daß das Resultat stimmt:

    ((\x ->[1,x]) >=>  _ ) 5    ===>   [4,2,8,2]

    Prüfen Sie, daß (>=>) assoziativ ist

  8. (Java) die Bedarfsauswertung eines Streams durch Stream.allMatch, Stream.anyMatch vorführen.

    In Haskell: all (\x -> x) [True,False, undefined] (keine Expection)

    In Java nicht so einfach, weil Stream.of(false,true,false).allMatch(x->x) alle Elemente schon bei Konstruktion auswertet.

    Ansatz: für eine Funktion f mit einer Nebenwirkung (Ausgabe auf Konsole) wird ausgewertet: Stream.of(...).map(f).allMatch(x->x)

    Dabei f als anonyme Funktion schreiben: _.map(x -> { ... ; return x })

  9. (C#) (siehe kw27/P.cs im Repo, korrigierte Version des Beispiels aus der VL)

    Func<int,bool> p = (x) => { for(int t = 2; t*t<=x; t++){if (0 == x % t) return false;} return x>=2; }

Time(()=> print (Enumerable.Range(0, 10000000).Where(p).Count()));

    1. ausführen, .AsParallel() an der passenden Stelle einfügen, ausführen, Lauzeiten vergleichen.

    2. die ausgebenen Zahlen auch vergleichen, untereinander und mit einer verläßlichen Quelle für die Anzahl der Primzahlen \(\le 10^n\).

    3. Dieser Primzahltest p verwendet Zustandsänderung und händischer Programmablaufsteuerung. Geben Sie einen rein funktionalen Test mit bedarfsausgewertetem Stream an. Ergänzen Sie:

      Func<int,bool> q = (x) => x >= 2 && Enumerable.Range(...).TakeWhile(...).All(...)

Ausblick, Zusammenfassung

Imperativ/Funktional (Beispiel)

Beispiel: Einfügen in Baum

Beispiel: unbalancierter Suchbaum

Größen-balancierter Suchbaum

Massen-Operationen mit Suchbäumen

Aufgabe zu Data.Set.intersection

Ausdrucksstarke Typen

Geschenkte Theoreme (free theorems)

Ausdrucksstärkere Typen: Balance

Daten-abhängige Typen (dependent types)

Wie weiter?

Zusammenfassung: Themen

Aussagen

Programmierer(in) sollte