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)

Klassische Implementierung von Mergesort

sort :: Ord a => [a] -> [a]
sort [] = [] ; sort [x] = [x]
sort xs =  let ( left,right ) = split xs
               sleft  = sort left  
               sright = sort right 
           in  merge sleft sright

wird parallelisiert durch Annotationen:

  sleft  = sort left  
              `using` rpar `dot` spineList
  sright = sort right `using` spineList

vgl. http://thread.gmane.org/gmane.comp.lang.haskell.parallel/181/focus=202

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

Softwaretechnische Aspekte

Literatur (allgemein)

Literatur (speziell diese VL)

Alternative Quellen

Organisation der LV

Hinweise zu Fernlehre

Übungen

Aufgaben

(im SS21: Aufgaben 2, 3 bis KW 15)

  1. 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?

  2. 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?

  3. Ü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.

  4. 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 (unsinnigerweise) 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)

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

Algebraische Datentypen

data Foo = Foo { bar :: Int, baz :: String } 
    deriving Show

Bezeichnungen (benannte Notation)

x :: Foo
x = Foo { bar = 3, baz = "hal" }

Bezeichnungen (positionelle Notation)

data Foo = Foo Int String  
y = Foo 3 "bar"

Datentyp mit mehreren Konstruktoren

Beispiel (selbst definiert)

data T = A { foo :: Int } 
       | B { bar :: String, baz :: Bool } 
    deriving Show

Bespiele (in Prelude vordefiniert)

data Bool = False | True
data Ordering = LT | EQ | GT

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

data Tree = Leaf {}
    | Branch { left :: Tree
             , right :: Tree }

Übung: Objekte dieses Typs erzeugen

(benannte und positionelle Notation der Konstruktoren)

Daten mit Baum-Struktur

Übung Terme

mit ghci:

Die Größe eines Terms \(t\) ist definiert durch

\(|f(t_0,\ldots,t_{k-1})| = 1 + \sum_{i=0}^{k-1} |t_i|\).

Hausaufgaben

SS21: für KW15: Aufgaben 2 und 3

  1. autotool-Aufgabe Data-1

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

    • 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 (eine data-Deklaration) mit genau 100 Elementen an. Sie können andere Data-Deklarationen benutzen (wie in autotool-Aufgabe). Minimieren Sie die Gesamtzahl aller deklarierten Konstruktoren.

  3. Vervollständigen Sie die Definition der Tiefe von Termen:

    \[\begin{aligned} && \operatorname{depth}( f() ) = 0 \\ k>0 &\Rightarrow& \operatorname{depth}(f(t_0,\ldots,t_{k-1})) = \dots\end{aligned}\]

    • Bestimmen Sie \(\operatorname{depth}(\sqrt{a\cdot a + b\cdot b})\)

    • Beweisen Sie \(\forall \Sigma: \forall t\in\operatorname{Term}(\Sigma): \operatorname{depth}(t) \le |t|-1\).

    • Für welche Terme gilt hier die Gleichheit?

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)

-- nicht disjunkt:
case t of { F (B x) y -> .. ; F x (B y) -> .. }
-- nicht vollständig:
case t of { F x y -> .. ; A -> .. }

data und case

typisches Vorgehen beim Verarbeiten algebraischer Daten vom Typ T:

Pattern Matching in versch. Sprachen

Nicht verwechseln mit regular expression matching zur String-Verarbeitung. Es geht um algebraische (d.h. baum-artige) Daten!

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

Notation für Termersetzungsregeln: anstatt \((l,r)\) schreibe \(l\to r\).

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)

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

Übung Pattern Matching, Programme

Hausaufgaben

im SS 21: Aufgaben 1 bis 4

  1. 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.

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

  3. für selbst definierte Wahrheitswerte

    deklarieren, implementieren und testen Sie die einstellige Negation, die zweistellige Antivalenz.

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

    Definieren Sie

    • not mit einer Gleichung (evtl. mit case)

    • xor ohne case (evtl. mehrere Gleichungen)

  4. 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 gerade Anzahl von Blättern enthält.

    Diese Anzahl nicht ausrechnen, sondern direkt den Wahrheitswert!

    Bemerkung zur Bezeichnung: man könnte auch

    data Node = Leaf | Branch Tree Tree

    schreiben, aber bitte niemals:

    data Tree = Leaf | Node Tree Tree

    denn auch Blätter sind Knoten (nodes)! Ein Branch ist ein Verzweigungsknoten oder innerer Knoten, ein Blatt ist ein äußerer Knoten des Baumes.

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

Beispiel Konstruktion/Induktion: even

Beispiel Konstruktion/Induktion: even (IA)

Beispiel Konstruktion/Induktion: even (IS)

Induktion über Bäume (IA)

Induktion über Bäume (IS)

Multiplikation von Peano-Zahlen

Subtraktion

Hausaufgaben

im SS21: Aufgaben 2 bis 5

  1. (autotool) 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 Bezeichnungnen für die Beweis-Schritte, geben Sie IA, IV, IB explizit an.

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

  3. Für zweistelliges min und max auf \(\NN\):

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

    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

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

Polymorphie

Definition, Motivation

Beispiele f. Typkonstruktoren (I)

Beispiele f. Typkonstruktoren (II)

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 (II)

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

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

    1. Maybe (Maybe Bool)

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

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

    4. geben Sie einen Typ mit 100 (Zusatz: 1000) Elementen an und (insgesamt) wenig Daten-Konstruktoren. (Vgl. frühere Aufgabe, die Frage ist jetzt, ob die Polymorphie hilft, eine kleinere Lösung zu erhalten)

  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)

  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. (von 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.

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

Falsches Binden lokaler Variablen

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

Umbenennung von lokalen Variablen

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

Übung Lambda-Kalkül

Hausaufgaben

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

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

    Normalform bestimmen: 1. auf Papier, 2. mit ghci.

    let t = \ f x -> f (f x)
...

    möglichst kleine Lambda-Ausdrücke (vom Typ N) angeben (Variablen, Applikation, Abstraktion, Konstruktoren von data N, keine Funktionen wie plus, mal), die eine große Normalform haben (mit ghci ausrechnen)

  3. 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

    • (autotool) Reduktionen im Lambda-Kalkül

L-K.: statische Semantik (Typisierung)

Motivation, Plan

Grundlagen zur Typisierung

Einfache (monomorphe) Typen

Typ-Abstraktion und -Applikation

Polymorphie: Notation

Polymorphie: Notation: Abkürzungen

Verkürzte Notation für Typen

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

im SS 21: Aufgaben 1, 3, 4, 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)\)

    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

    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. die Funktionen partition, span

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

    2. die API-Dokumentation aufsuchen (hackage.org)

    3. die dort angegebenen Eigenschaften als Leancheck-Property überprüfen

    4. die entsprechenden Funktionen aus Data.Sequence aufrufen

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

Rekursionsschema f. mehrstellige Fkt.

Rekursionsmuster (Peano-Zahlen)

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

Rekursionsmuster für Bäume (Bsp. 2)

Übung Rekursionsmuster

Implementierungen für natürlichen Zahlen

Merksätze

Hausaufgaben für KW 22

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

    • Bool

    • Maybe a

    • Pair a b

    • Either a b

    Jeweils:

    • Typ und Implementierung (vorbereiteten Quelltext zeigen)

    • Testfälle (in ghci vorführen)

    • gibt es diese Funktion bereits? Suchen Sie nach dem Typ mit https://www.haskell.org/hoogle/

  2. Rekursionsmuster auf Peano-Zahlen

    • plus, mal, hoch vorführen (jeweils realisiert als fold)

      Testen Sie mit Leancheck einige Eigenschaften.

    • 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)

  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.

      (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.

Eingeschränkte Polymorphie

Typklassen in Haskell: Überblick

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]

Grundwissen Typklassen

Typklassen in Bibliotheks-Schnittstellen

(Eingeschränkt) polymorphe Literale

Unterschiede Typklasse/Interface (Bsp)

Unterschiede Typklasse/Interface (Impl.)

Typklassen/Interfaces: Vergleich

Generische Instanzen (I)

class Eq a where
    (==) :: a -> a -> Bool

Vergleichen von Listen (elementweise)

wenn a in Eq, dann [a] in Eq:

instance Eq a => Eq [a] where
  l == r = case l of
    [] -> case r of
      [] -> True ; y : ys -> False
    x : xs -> case r of
      [] -> False 
      y : ys -> (x == y) && ( xs == ys )

Übung: wie sieht instance Ord a => Ord [a] aus? (lexikografischer Vergleich)

Generische Instanzen (II)

class Show a where
  show ::  a -> String
instance Show Bool where
  show False = "False" ; show True = "True"
instance Show a => Show [a] where
  show xs = brackets 
          $ concat
          $ intersperse "," 
          $ map show xs
instance (Show a, Show b) => Show (a,b) where ...
show False = "False"
show ([True,False],True) 
  = "([True,False],True)"

Benutzung von Typklassen bei Leancheck

Test.LeanCheck—Beispiel

Testen für beliebige Stelligkeit

Überblick über Leancheck-Implementierung

Hausaufgaben

  1. definieren Sie für data T = T Bool Bool Bool

    • instance Eq als komponentenweise Gleichheit

    • instance Ord als lexikografische Erweiterung der Standard-Ordnung auf Bool

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

    • transitiv

    • antisymmetrisch

    ist und prüfen Sie das für Numeric.Natural und für T.

    transitiv :: Ord a => a -> a -> a -> Bool
check (transitiv @T)

  2. definieren Sie für data T = T Bool Bool Bool

    • instance Semigroup als komponentenweise Disjunktion

    • instance Monoid als dazu passendes neutrales Element

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

    Geben Sie eine korrekte Monoid-Struktur für T an, die nicht kommutativ ist.

  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 das Typconstraint (oder dessen Fehlen) für singleton.

    für Data.Map:

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

    • Definieren Sie einen Typ data T = ... deriving Eq und dafür eine Ord-Instanz, die keine totale Ordnung definiert.

      Zeigen Sie durch Beispiele, daß dann M.Map T v nicht funktioniert. Z.B.: eingefügter Schlüssel nicht in M.toList, sichtbarer Schlüssel nicht gefunden.

Verzögerte Auswertung (lazy evaluation)

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 Nat ; nf :: Nat -> Stream Nat
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.: Modularität

Anwendg. Lazy Eval.: Streams

unendliche Datenstrukturen

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

für SS21: Aufgaben 1 bis 3 auf jeden Fall, und eine von 4 und 5

  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

    Bereiten Sie (wenigstens) 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) mit Rekursion:

    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 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

Verbrauch von Datenströmen: Fold

Wiederholung, Motivation

Fold-Left: Beispiel

Fold-Left: Implementierung

Fold-Left: allgemeiner Typ

Das strikte Fold-Left: Anwendung

Fold-Left mit nicht-striktem Argument

Transformation von Datenströmen

Bsp: Linq (Language integrated query) in C#

Kombination von Strömen mit SelectMany

Anwendung von Bind

do-Notation

Wdhlg: der Typkonstruktor Maybe

Die Konstruktorklasse Monad

Axiome für Monaden

Maybe als Monade

IO: die Schnittstelle zum Betriebssystem

Maybe in C# (Nullable)

Nullable als Monade

Übungen zu Monaden

  1. (wurde in der VL vorgeführt) Testen der Monaden-Axiome für Maybe in ghci:

    import Test.LeanCheck
import Test.LeanCheck.Function

f >=> g = \ x -> f x >>= g

check $ \ f x -> 
   ((f :: Bool -> Maybe Int) >=> return) x == f x

    beachten Sie

Hausaufgaben

SS 21: Aufgaben 1, 2, 4, 5.

  1. 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, rechts nicht p x && q x schreiben darf.

    Warum—die Konjunktion ist doch kommutativ?

    Hinweis: auf Bool ja, auf \(\texttt{Bool}_\bot\) nicht.

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

  3. für instance Monad Maybe: zeigen Sie, daß (>=>) nicht kommutativ ist.

    Geben Sie einen statisch korrekten Testfall an, für den der kommutierte (vertauschte) Ausdruck statisch falsch (typfehlerhaft) ist.

    Geben Sie Testfälle an, bei denen die Kommutation statisch korrekt ist, aber die dynamische Semantik (die berechneten Werte) nicht übereinstimmen.

    Verwenden Sie dafür Leancheck.

  4. zur Listen-Monade:

    Erfüllt die folgende Instanz die Monaden-Axiome?

    return x = [x]
xs >>= f = take 2 (concat (map f xs))

    Hinweis: import Prelude hiding ((>>=)), dann (>>=) wie hier. return wird unverändert importiert.

    Definieren Sie den Operator f >=> g = \ xs -> f xs >>= g, testen Sie die Axiome mittels Leancheck.

  5. Maybe in C# und Java:

    • Nullable<T> in C# Ist ?? tatsächlich assoziativ? Vergleichen Sie die Bedeutung von (a ?? b) ?? c und a ?? (b ?? c) unter diesen Aspekten:

      • statische Semantik: Typisierung

      • dynamische Semantik: einschließlich \(\bot\) (Exceptions)

    • Optional<T> in Java:

      • welche Methoden realisieren bind und return?

      • was entspricht dem Operator ?? aus C#?

    Primär-Quellen (Dokumentation) angeben, Rechnungen in csharp (mono) bzw. jshell (jdk) vorführen.

  6. (mglw. autotool—CYP) beweisen Sie diese Beziehung zwischen foldl und foldr

    foldl :: (b -> a -> b) -> b -> [a] -> b
foldl f z0 xs =
  let f' x k z = k (f z x)
  in  foldr f' id xs z0

  7. (später) definieren Sie eine Monad-Instanz jeweils für

    • binäre Bäume mit Schlüsseln nur in den Blättern

    • …nur in den Verzweigungsknoten

    • …in allen Knoten

    • beliebig verzweigende Bäume rose trees data Tree a = Node a [Tree a]

    überprüfen Sie ein Einhaltung der Axiome.

Unveränderliche Daten

Überblick

Beispiel: Einfügen in Baum

Beispiel: unbalancierter Suchbaum

Löschen in unbalancierten Suchbäumen

Größen-balancierter Suchbaum

Persistente Objekte in Git

Objekt-Versionierung in Git

Theorems for Free: Beispiel

Theorems for Free: Quelle

Struktur-erhaltende Transformationen

Theorems for Free: Systematik, Beispiele

Freie Theoreme für Funktions-Typen

Hausaufgaben

SS21: Aufgaben 1, 2, 4, 5.

  1. für \(\alpha\)-balancierte Suchbäume

    • Geben Sie einen \(1/4\)-balancierten Baum mit (z.B.) 10 Schlüsseln an, der möglichst hoch ist. In jedem Branch l k r soll \(|l|\le |r|\) gelten.

      Vergleichen Sie die Höhe mit der in der VL berechneten Schranke.

    • Vergleichen Sie die Implementierung von split und (z.B.) union (Fig. 1 des zitierten Papers) mit der Implementierung der entsprechenden Funktion aus https://hackage.haskell.org/package/containers-0.6.4.1/docs/Data-Set.html

    • für Data.Set: erläutern Sie Laufzeit-Unterschiede zwischen fromList und fromAscList

  2. Für rose trees (Rhododendron)

    data Tree k = Node k [Tree k]

    • Implementieren Sie das Rekursionsschema

      fold :: (k -> [res] -> res) -> Tree k -> res

      (dieser Typ war ursprünglich fehlerhaft angegeben, wurde repariert Mon 28 Jun 2021 11:46:24 CEST)

    • Bestimmen Sie mit diesem fold die Anzahl der Knoten, die Höhe, die Summe der Schlüssel.

    • Konstruieren Sie Binomialbäume:

      \(B_n\) hat Schlüssel \(n\) und Kinder \([B_0, \ldots, B_{n-1}]\)

      insbesondere: \(B_0\) hat Schlüssel 0 und keine Kinder.

    • berechnen Sie die o.g. Parameter für kleine \(B_n\), geben Sie allgmeine Aussagen (für alle \(B_n\) an), beweisen Sie diese.

  3. git bisect erläutern und vorführen. Dazu ein überschaubares kleines Projekt verwenden (oder anlegen) (ca. 10 commits) mit einfachem Testfall sowie einem einfachen Fehler irgendwo.

    In diesem Zusammenhang Verhaltensregeln/Empfehlungen diskutieren (master always buildable, squash commits?)

  4. instance Functor Tree

    • implementieren Sie die Functor-Instanz für

      binäre Bäume mit Schlüsseln in inneren Knoten

      (1. mit Rekursion, 2. mit fold)

    • überprüfen Sie die Axiome für fmap

      Benutzen Sie Aufzählung von Funktionen in Leancheck

    • geben Sie das freie Theorem für den Typ

      1. Tree k -> [k], 2. Tree k -> Nat

      an und überprüfen Sie an Beispielen

  5. Freie Theoreme gibt es nur für uneingeschränkt polymorphe Typen. Für Typen mit Constraints

    Bsp. Data.List.sort :: Ord k => [k] -> [k]

    betrachtet man stattdessen die Funktion, bei der das Typconstraint durch das Wörterbuch-Argument (hier: mit der einzigen Funktion compare) ersetzt wird.

    Für dieses Beispiel ist das Data.List.sortBy. Geben Sie für deren Typ das freie Theorem an, überprüfen Sie.

    (nächste Teilaufgabe hat nichts mit freien Theoremen zu tun. Beachten Sie: wer außerhalb einer Übungsaufgabe sortiert, macht einen Fehler, hätte stattdessen Data.Set benutzen sollen. Wer einfach verkettete Listen benutzt, auch (\(\Rightarrow\) Data.Sequence, Data.Vector). Wer Strings benutzt, auch (\(\Rightarrow\) Data.Text))

    Wenn man bezüglich einer bestimmten Maßfunktion sortieren möchte, z.B. Strings nach der Länge, dann kann man verwenden

    import Data.Function (on)
sortBy (compare `on` length) ["fooo", "bar", ""]

    aber auch

    sortOn length ["fooo", "bar", ""]

    Erklären Sie `on`. Erklären Sie den Unterschied (Laufzeit, Platz) zwischen beiden Varianten.

Zusammenfassung, Ausblick

Zusammenfassung, Ausblick

Prüfungen

Hausaufgaben für Übung KW 27

Erläuterung/Wiederholung: Currying

Erläuterung/Wiederholung: Extensionalität

Wiederholung/Bsp: generische Polymorphie

Zusammenfassung: Themen

Aussagen

Programmierer(in) sollte

Zur objektorientierten Programmierung

Ausdrucksstarke Typen

Ausdrucksstärkere Typen: Balance

Daten-abhängige Typen (dependent types)