commit 3224d100da12d15e782592713c930aa4b9866cc3 Author: Markus Birth Date: Sat Oct 19 01:17:37 2013 +0200 Initial commit diff --git a/Blatt01/Example.impl b/Blatt01/Example.impl new file mode 100644 index 0000000..3f21e34 --- /dev/null +++ b/Blatt01/Example.impl @@ -0,0 +1,6 @@ +IMPLEMENTATION Example + +IMPORT Nat COMPLETELY + +DEF incdec == \\x . (x + 1, x - 1) + diff --git a/Blatt01/Example.sign b/Blatt01/Example.sign new file mode 100644 index 0000000..431fa06 --- /dev/null +++ b/Blatt01/Example.sign @@ -0,0 +1,6 @@ +SIGNATURE Example + +IMPORT Nat ONLY nat + +FUN incdec : nat -> nat ** nat + diff --git a/Blatt01/Fac.impl b/Blatt01/Fac.impl new file mode 100644 index 0000000..2b98c8e --- /dev/null +++ b/Blatt01/Fac.impl @@ -0,0 +1,4 @@ +IMPLEMENTATION Fac + +IMPORT Nat COMPLETELY + diff --git a/Blatt01/Fac.sign b/Blatt01/Fac.sign new file mode 100644 index 0000000..2f9dbe3 --- /dev/null +++ b/Blatt01/Fac.sign @@ -0,0 +1,4 @@ +SIGNATURE Fac + +IMPORT Nat ONLY nat + diff --git a/Blatt01/Geometry.impl b/Blatt01/Geometry.impl new file mode 100644 index 0000000..3d87ccb --- /dev/null +++ b/Blatt01/Geometry.impl @@ -0,0 +1,10 @@ +IMPLEMENTATION Geometry + +IMPORT Real COMPLETELY + +DEF square == \\x. x*x + +DEF cube == \\x . x*x*x + +DEF rectArea == \\l,w . l*w + diff --git a/Blatt01/Geometry.sign b/Blatt01/Geometry.sign new file mode 100644 index 0000000..5b730da --- /dev/null +++ b/Blatt01/Geometry.sign @@ -0,0 +1,23 @@ +SIGNATURE Geometry + +IMPORT Real ONLY real + +/* Liefert den Quadrat einer Zahl. */ +FUN square : real -> real + +/* Liefert den Kubus einer Zahl. */ +FUN cube : real -> real + +/* Liefert die Flaeche eines Rechtecks mit der gegebenen Laenge und Breite. + Die Funktion akzeptiert nur positive Zahlen. */ +FUN rectArea : real ** real -> real + +/* Liefert die Laenge einer Hypotenuse in einem rechtwinkligen Dreieck mit + den gegebenen Laengen der Katheten. Die Funktion akzeptiert nur positive + Zahlen. */ +FUN hypot : real ** real -> real + +/* Liefert das Volumen eines Quaders mit der gegebenen Laenge, Breite und + Hoehe. Die Funktion akzeptiert nur positive Zahlen. */ +FUN cuboidVolume : real ** real ** real -> real + diff --git a/Blatt01/blatt1.pdf b/Blatt01/blatt1.pdf new file mode 100644 index 0000000..3ac8db6 Binary files /dev/null and b/Blatt01/blatt1.pdf differ diff --git a/Blatt02/Recursion.impl b/Blatt02/Recursion.impl new file mode 100644 index 0000000..a5f9b89 --- /dev/null +++ b/Blatt02/Recursion.impl @@ -0,0 +1,64 @@ +IMPLEMENTATION Recursion + +IMPORT Nat COMPLETELY +IMPORT Denotation COMPLETELY +IMPORT Char COMPLETELY + +DEF plus == \\m,n . IF n = 0 + THEN m + ELSE plus(succ(m), pred(n)) + FI + +DEF sum == \\m,n. IF m>n THEN 0 + ELSE m + sum(m+1,n) + FI + +DEF in? == \\c,d. IF d = "" THEN false + ELSE IF d ! 0 = c THEN true + ELSE in?(c,delete(d,0,0)) + FI + FI + +DEF mult == \\a,b. IF a>0 THEN b+mult(a-1,b) ELSE 0 FI +/* Alternativ: IF a>1 THEN b+mult(a-1,b) ELSE b FI */ + +DEF sumEven == \\m,n. IF m>n THEN 0 + ELSE IF m%2=0 THEN m + sumEven(m+1,n) + ELSE sumEven(m+1,n) FI FI + +DEF count == \\c,d. IF d = "" THEN 0 + ELSE IF d ! 0 = c THEN 1+count(c,delete(d,0,0)) + ELSE count(c,delete(d,0,0)) FI FI + +DEF countDigits == \\d. IF d = "" THEN 0 + ELSE IF digit?(d!0) THEN 1+countDigits(delete(d,0,0)) + ELSE countDigits(delete(d,0,0)) FI FI + + + +/* TUT-Examples following */ + +FUN h : nat ** nat -> nat ** nat +DEF h == \\m,n. (h1(m,n), h2(m,n)) + +FUN h1 : nat ** nat -> nat +DEF h1 == \\m,n. IF m < n THEN 0 ELSE h1(m-n,n) + 1 FI + +FUN h2 : nat ** nat -> nat +DEF h2 == \\m,n. IF m < n THEN m ELSE h2(m-n,n) FI + + +FUN f : nat ** nat -> nat +DEF f == \\a,b. IF a > b THEN f1(a,b,a) + ELSE f1(b,a,b) + FI + +FUN f1 : nat ** nat ** nat -> nat +DEF f1 == \\a,b,z. IF mod(a,b) = 0 THEN a + ELSE f1(a+z,b,z) + FI + +FUN g : nat ** nat -> nat +DEF g == \\a,b. IF b = 0 THEN a + ELSE g(b,mod(a,b)) + FI diff --git a/Blatt02/Recursion.sign b/Blatt02/Recursion.sign new file mode 100644 index 0000000..c6d4335 --- /dev/null +++ b/Blatt02/Recursion.sign @@ -0,0 +1,27 @@ +SIGNATURE Recursion + +IMPORT Nat ONLY nat +IMPORT Denotation ONLY denotation +IMPORT Char ONLY char + +/* Addiert zwei natuerliche Zahlen */ +FUN plus : nat ** nat -> nat + +/* Multipliziert zwei natuerliche Zahlen */ +FUN mult : nat ** nat -> nat + +/* Liefert die Summe aller natuerlichen Zahlen zwischen den zwei Zahlen */ +FUN sum : nat ** nat -> nat + +/* Liefert die Summe aller GERADEN natuerlichen Zahlen zw. den zwei Zahlen */ +FUN sumEven : nat ** nat -> nat + +/* Liefert true, wenn char in denotation vorkommt, sonst false */ +FUN in? : char ** denotation -> bool + +/* Liefert die Vorkommen von char in denotation */ +FUN count : char ** denotation -> nat + +/* Liefert die Anzahl von Ziffern in einer denotation */ +FUN countDigits : denotation -> nat + diff --git a/Blatt02/Solve.impl b/Blatt02/Solve.impl new file mode 100644 index 0000000..7ecb616 --- /dev/null +++ b/Blatt02/Solve.impl @@ -0,0 +1,27 @@ +IMPLEMENTATION Solve + +IMPORT Real COMPLETELY +IMPORT BOOL ONLY true false + +DEF triangleArea == \\a,b,c. LET + s == (a+b+c)/2 + IN + sqrt(s * (s-a) * (s-b) * (s-c)) + +DEF qsolve == \\o,p,q. + IF o |= 0 + THEN (0-(p/(2*o))+sqrt(((p/(2*o)) pow 2)-(q/o)),0-(p/(2*o))-sqrt(((p/(2*o)) pow 2)-(q/o))) + FI + +DEF qunique? == \\o,p,q. + LET (a, b) == qsolve(o,p,q) + IN + IF a=b + THEN true ELSE false + FI + +DEF qunique2? == \\o,p,q. + IF a=b + WHERE (a,b) == qsolve(o,p,q) + THEN true ELSE false + FI diff --git a/Blatt02/Solve.sign b/Blatt02/Solve.sign new file mode 100644 index 0000000..cc1da34 --- /dev/null +++ b/Blatt02/Solve.sign @@ -0,0 +1,21 @@ +SIGNATURE Solve + +IMPORT Real ONLY real +IMPORT BOOL ONLY bool + +FUN triangleArea : real ** real ** real -> real + +/* Rechnet die zwei Nullstellen einer quadratischen Gleichung aus + Syntax: qsolve(a,b,c) + für eine Gleichung der Form ax²+bx+c + Liefert: (n,m) = die beiden Nullstellen */ +FUN qsolve : real ** real ** real -> real ** real + + +/* Prüfen, ob eine quadratische Gleichung nur 1 Lösung hat. + Syntax: qunique[2]?(a,b,c) + für eine Gleichung in der Form ax²+bx+c + a darf NICHT 0 sein + Liefert: Boolean true oder false */ +FUN qunique? : real ** real ** real -> bool +FUN qunique2? : real ** real ** real -> bool diff --git a/Blatt02/blatt2.lsg.pdf b/Blatt02/blatt2.lsg.pdf new file mode 100644 index 0000000..9bc9174 Binary files /dev/null and b/Blatt02/blatt2.lsg.pdf differ diff --git a/Blatt02/blatt2.pdf b/Blatt02/blatt2.pdf new file mode 100644 index 0000000..036b529 Binary files /dev/null and b/Blatt02/blatt2.pdf differ diff --git a/Blatt03/MergeSort.impl b/Blatt03/MergeSort.impl new file mode 100644 index 0000000..6c9125e --- /dev/null +++ b/Blatt03/MergeSort.impl @@ -0,0 +1,22 @@ +IMPLEMENTATION MergeSort + +IMPORT Real COMPLETELY +IMPORT Seq[nat] COMPLETELY + +-- Unsortierte Sequenz zu Testzwecken +FUN testSeq : seq[nat] +DEF testSeq == %(5,7,6,4,8,3,9,2) ++ %(0,1,10) + +DEF mergeSort(<>) == <> +DEF mergeSort(::(a,s)) == IF <>?(s) THEN ::(a,<>) + ELSE LET(s1,s2) == split(::(a,s)) + IN merge(mergeSort(s1),mergeSort(s2)) FI + +FUN split : seq[nat] -> seq[nat]**seq[nat] +DEF split(<>) == (<>, <>) +DEF split(n::ns) == LET (s1,s2) == split(ns) IN (s2,n::s1) + +FUN merge : seq[nat]**seq[nat] -> seq[nat] +DEF merge(<>,s) == s +DEF merge(s,<>) == s +DEF merge(s1,s2) == IF ft(s1) > ft(s2) THEN ft(s2)::merge(s1,rt(s2)) ELSE ft(s1)::merge(rt(s1),s2) FI diff --git a/Blatt03/MergeSort.impl2 b/Blatt03/MergeSort.impl2 new file mode 100644 index 0000000..6c84fe9 --- /dev/null +++ b/Blatt03/MergeSort.impl2 @@ -0,0 +1,45 @@ +IMPLEMENTATION MergeSort + +IMPORT Nat COMPLETELY +IMPORT Seq[nat] COMPLETELY + +-- Unsortierte Sequenz zu Testzwecken +FUN testSeq : seq[nat] +DEF testSeq == %(5,7,6,4,8,3,9,2) ++ %(0,1,10) + +-- Sortiert die übergebene Sequenz mit Hilfe des Sortier- +-- verfahrens MergeSort +FUN mergeSort : seq[nat] -> seq[nat] +DEF mergeSort == \\ s . + IF <>?(s) THEN <> + -- leere Liste sortieren + OTHERWISE + IF <>?(rt(s)) THEN ft(s) :: <> + -- einelementige Liste sortieren + ELSE LET (s1,s2) == split(s) + IN merge(mergeSort(s1),mergeSort(s2)) + -- andere Listen sortieren + FI + +-- Splittet eine Liste in zwei Listen +FUN split : seq[nat] -> seq[nat] ** seq[nat] +DEF split(<>) == + (<>, <>) +DEF split(x::xs) == + LET (s1, s2) == split(xs) + IN (s2, x::s1) + +-- Fuegt zwei sortierte Listen zusammen +FUN merge : seq[nat] ** seq[nat] -> seq[nat] +DEF merge == \\ s1,s2 . + IF <>?(s1) THEN s2 + IF <>?(s2) THEN s1 + OTHERWISE + IF ft(s1) > ft(s2) THEN ft(s2) :: merge(s1,rt(s2)) + -- erste Element der zweiten Liste ist kleiner oder gleich + ELSE ft(s1) :: merge(rt(s1),s2) + -- erste Element der ersten Liste ist kleiner + FI + +-- Testen mit e mergeSort(testSeq) +-- Ergebnis ist dann <0,1,2,3,4,5,6,7,8,9,10> diff --git a/Blatt03/MergeSort.sign b/Blatt03/MergeSort.sign new file mode 100644 index 0000000..75f3252 --- /dev/null +++ b/Blatt03/MergeSort.sign @@ -0,0 +1,8 @@ +SIGNATURE MergeSort + +IMPORT Nat COMPLETELY +IMPORT Seq[nat] COMPLETELY + +-- Sortiert die übergebene Sequenz mit Hilfe des Sortier- +-- verfahrens MergeSort +FUN mergeSort : seq[nat] -> seq[nat] diff --git a/Blatt03/MergeSort.sign2 b/Blatt03/MergeSort.sign2 new file mode 100644 index 0000000..75f3252 --- /dev/null +++ b/Blatt03/MergeSort.sign2 @@ -0,0 +1,8 @@ +SIGNATURE MergeSort + +IMPORT Nat COMPLETELY +IMPORT Seq[nat] COMPLETELY + +-- Sortiert die übergebene Sequenz mit Hilfe des Sortier- +-- verfahrens MergeSort +FUN mergeSort : seq[nat] -> seq[nat] diff --git a/Blatt03/QuickSort.impl b/Blatt03/QuickSort.impl new file mode 100644 index 0000000..5aea5fd --- /dev/null +++ b/Blatt03/QuickSort.impl @@ -0,0 +1,15 @@ +IMPLEMENTATION QuickSort + +IMPORT Nat COMPLETELY +IMPORT Seq[nat] COMPLETELY + +-- Unsortierte Sequenz zu Testzwecken +FUN testSeq : seq[nat] +DEF testSeq == %(5,7,6,4,8,3,9,2) ++ %(0,1,10) + +DEF quickSort(<>) == <> +DEF quickSort(a::R) == LET sm == (_ < a)|R + me == a :: (_ = a)|R + la == (_ > a)|R + IN quickSort(sm) ++ me ++ quickSort(la) + diff --git a/Blatt03/QuickSort.sign b/Blatt03/QuickSort.sign new file mode 100644 index 0000000..7f63108 --- /dev/null +++ b/Blatt03/QuickSort.sign @@ -0,0 +1,8 @@ +SIGNATURE QuickSort + +IMPORT Nat COMPLETELY +IMPORT Seq[nat] COMPLETELY + +-- Sortiert die übergebene Sequenz mit Hilfe des Sortier- +-- verfahrens QuickSort +FUN quickSort : seq[nat] -> seq[nat] diff --git a/Blatt03/Sequences.impl b/Blatt03/Sequences.impl new file mode 100644 index 0000000..e4f120b --- /dev/null +++ b/Blatt03/Sequences.impl @@ -0,0 +1,16 @@ +IMPLEMENTATION Sequences + +IMPORT Nat COMPLETELY +IMPORT Seq[nat] COMPLETELY +IMPORT Real COMPLETELY +IMPORT Seq[real] COMPLETELY + +DEF scalar == \\s1,s2 . IF <>?(s1) THEN 0 ELSE IF <>?(s2) THEN 0 ELSE ft(s1)*ft(s2)+scalar(rt(s1),rt(s2)) FI FI + +DEF genList == \\n . IF n=0 THEN <> ELSE n::genList(n-1) FI + +DEF horner == \\k,x . LET k1 == ft(k) + k2 == ft(rt(k)) + k3 == ft(rt(rt(k))) + k4 == ft(rt(rt(rt(k)))) + IN (((k1)*x+k2)*x+k3)*x+k4 diff --git a/Blatt03/Sequences.sign b/Blatt03/Sequences.sign new file mode 100644 index 0000000..5f52c82 --- /dev/null +++ b/Blatt03/Sequences.sign @@ -0,0 +1,19 @@ +SIGNATURE Sequences + +IMPORT Nat COMPLETELY +IMPORT Seq[nat] COMPLETELY +IMPORT Real COMPLETELY +IMPORT Seq[real] COMPLETELY + +/* Berechnet das Skalarprodukt zweier als Sequenzen uebergebener Vektoren + Die beiden Sequenzen sollten die gleiche Laenge haben */ +FUN scalar : seq[nat]**seq[nat] -> nat + + +/* Erzeugt eine Sequenz mit den Elementen 1..n oder eine leere Sequenz, wenn 0 uebergeben wird */ +FUN genList : nat -> seq[nat] + +/* Berechnet ein Polynom unter Verwendung des Horner-Schemas + Uebergeben werden hierbei die Koeffizienten (((a)*x+b)*x+c)*x+d als Sequenz und x als + zweiter Parameter */ +FUN horner : seq[real]**real -> real diff --git a/Blatt03/blatt3.lsg.pdf b/Blatt03/blatt3.lsg.pdf new file mode 100644 index 0000000..783ec9c Binary files /dev/null and b/Blatt03/blatt3.lsg.pdf differ diff --git a/Blatt03/blatt3.pdf b/Blatt03/blatt3.pdf new file mode 100644 index 0000000..dadadfc Binary files /dev/null and b/Blatt03/blatt3.pdf differ diff --git a/Blatt04/Blatt4.impl b/Blatt04/Blatt4.impl new file mode 100644 index 0000000..28e440a --- /dev/null +++ b/Blatt04/Blatt4.impl @@ -0,0 +1,253 @@ +IMPLEMENTATION Blatt4 + +IMPORT Nat COMPLETELY + Seq COMPLETELY + + +-- Aufgabe 1 ------------------------------------------------------------------ + +-- Aufgabe 1.1 ---------------------------------------------------------------- + +/* +-- nicht optimierte Variante +FUN primeFactorDecomposition: nat -> seq[nat] +DEF primeFactorDecomposition(n) == primeFactors(2, n) + +-- primeFactors(k, n) berechnet die Sequenz der Primfaktoren +-- von n unter der Voraussetzung, daß n keine Primfaktoren +-- besitzt, die kleiner als k sind. +FUN primeFactors: nat ** nat -> seq[nat] +DEF primeFactors(k, n) == + IF n = 1 THEN <> + OTHERWISE + IF n%k = 0 THEN k :: primeFactors(k, n/k) + ELSE primeFactors(k+1, n) + FI +*/ + + +-- optimierte Variante +FUN primeFactorDecomposition: nat -> seq[nat] +DEF primeFactorDecomposition(n) == primeFactors(2, 1, n) + +-- primeFactors(k, step, n) berechnet die Sequenz der Primfaktoren +-- von n unter der Voraussetzung, daß n keine Primfaktoren +-- besitzt, die kleiner als k sind. +-- Dabei muß step=1 gelten, wenn k gerade ist +-- und step=2, wenn k ungerade ist. +-- (... eine derartige Funktion darf niemals eine "Benutzerfunktion" sein, +-- da derart seltsame Anwendungsbedingungen nur für eine Hilfsfunktion +-- akzeptabel sind) +FUN primeFactors: nat ** nat ** nat -> seq[nat] +DEF primeFactors(k, step, n) == + IF n = 1 THEN <> + OTHERWISE + IF n%k = 0 THEN k :: primeFactors(k, step, n/k) + ELSE primeFactors(k+step, 2, n) + FI + + +-- Aufgabe 1.2 ---------------------------------------------------------------- + +FUN ascendingPrefix: seq[nat] -> seq[nat] ** seq[nat] +DEF ascendingPrefix(S) == + IF S <>? THEN (<>,<>) + ELSE + LET + n == ft(S) + R == rt(S) + IN + IF R <>? THEN (S,<>) + OTHERWISE + IF n <= ft(R) THEN + (n::S1, S2) + WHERE + (S1, S2) == ascendingPrefix(R) + ELSE + (n::(<>), R) + FI + FI + + +-- Aufgabe 2 ------------------------------------------------------------------ + +-- Aufgabe 2.1 (Tut) ---------------------------------------------------------- + +FUN ascendingParts: seq[nat] -> seq[seq[nat]] +DEF ascendingParts(S) == + IF S <>? THEN <> + ELSE + LET + (part, rest) == ascendingPrefix(S) + IN + part :: ascendingParts(rest) + FI + + +-- Aufgabe 2.2 (Tut) ---------------------------------------------------------- + +/* +-- nicht optimierte Variante +FUN powerSet: seq[nat] -> seq[seq[nat]] +DEF powerSet == + \\S. IF S <>? THEN <> :: <> + ELSE + powerSubset ++ prepend(ft(S),powerSubset) + WHERE + powerSubset == powerSet(rt(S)) + FI +*/ + +-- prepend(n,S) stellt jeder in S enthaltenen Sequenz die Zahl n voran +FUN prepend: nat ** seq[seq[nat]] -> seq[seq[nat]] +DEF prepend == + \\n,S. IF S <>? THEN <> + ELSE (n::ft(S))::prepend(n,rt(S)) + FI + + +-- optimierte Variante +FUN powerSet: seq[nat] -> seq[seq[nat]] +DEF powerSet == + \\S. IF S <>? THEN <> :: <> + ELSE augment(ft(S),powerSet(rt(S))) + FI + +-- augment(n,S) = ( prepend(n,S) vereinigt mit S ) +FUN augment: nat ** seq[seq[nat]] -> seq[seq[nat]] +DEF augment == + \\n,S. IF S <>? THEN <> + ELSE (n::ft(S))::ft(S)::augment(n,rt(S)) + FI + + +-- Aufgabe 2.3 ---------------------------------------------------------------- + +FUN perm: seq[nat] -> seq[seq[nat]] +DEF perm == + \\S. IF S <>? THEN <> :: <> + ELSE insertInAllLists(ft(S),perm(rt(S))) + FI + +-- insertInAllLists(n,S) bildet für jede Sequenz von S alle möglichen +-- Zerlegungen in zwei Teile, fügt jeweils n dazwischen ein und liefert +-- alle resultierenden Sequenzen zurück. +FUN insertInAllLists: nat ** seq[seq[nat]] -> seq[seq[nat]] +DEF insertInAllLists == + \\n,S. IF S <>? THEN <> + ELSE insertAtAllPositions(n,ft(S)) + ++ insertInAllLists(n,rt(S)) + FI + +-- Für jede mögliche Zerlegung von S = S1.S2 erzeugt +-- insertAtAllPositions(n,S) die Sequenz S' = S1.n.S2 und liefert +-- alle diese Sequenzen zurück. +FUN insertAtAllPositions: nat ** seq[nat] -> seq[seq[nat]] +DEF insertAtAllPositions == + \\n,S. IF S <>? THEN (n :: <>) :: <> + ELSE (n :: S) :: prepend(ft(S),insertAtAllPositions(n,rt(S))) + FI + +-- Aufgabe 3 ------------------------------------------------------------------ + +-- zum Testen +FUN vec1: seq[nat] +DEF vec1 == %(1,2,3,4) + +FUN mat1 mat2: seq[seq[nat]] +DEF mat1 == %(%(1,2,3,4), + %(5,6,7,8), + %(9,10,11,12)) + +DEF mat2 == %(%(1,2,3), + %(4,5,6), + %(7,8,9), + %(10,11,12)) + +-- zur Kontrolle: + +-- mat1 * vec1 = <30,70,110> + +-- mat1 * mat2 = << 70, 80, 90>, +-- <158,184,210>, +-- <246,288,330>> + +-- mat2 * mat1 = << 38, 44, 50, 56>, +-- < 83, 98,113,128>, +-- <128,152,176,200>, +-- <173,206,239,272>> + + + +-- Funktionen höherer Ordnung dürft ihr in diesem Blatt noch nicht verwenden. +IMPORT SeqZip ONLY zip -- nur für das Skalarprodukt + SeqReduce ONLY / -- nur für das Skalarprodukt + +-- Skalarprodukt zweier Vektoren (gleicher Dimension) +FUN skalarProd: seq[nat] ** seq[nat] -> nat +DEF skalarProd(v1,v2) == (+,0) / zip(*)(v1,v2) + + +-- Aufgabe 3.1 (Tut) ---------------------------------------------------------- + +-- matVecProd(M,v) setzt voraus, daß die Anzahl der Spalten von M +-- gleich der Anzahl der Elemente (Zeilen) von v ist. +FUN matVecProd : seq[seq[nat]] ** seq[nat] -> seq[nat] +DEF matVecProd(M,v) == + IF M <>? THEN <> + ELSE skalarProd(ft(M),v) :: matVecProd(rt(M),v) + FI + + +-- Aufgabe 3.2 ---------------------------------------------------------------- + +FUN transp: seq[seq[nat]] -> seq[seq[nat]] +DEF transp(M) == + IF ft(M) <>? THEN <> + ELSE mapFt(M) :: transp(mapRt(M)) + FI + +-- Extraktion der ersten Spalte einer Matrix +FUN mapFt: seq[seq[nat]] -> seq[nat] +DEF mapFt(M) == + IF M <>? THEN <> + ELSE ft(ft(M)) :: mapFt(rt(M)) + FI + +-- Abschneiden der ersten Spalte einer Matrix +-- mit Rückgabe der verbleibenden Untermatrix +FUN mapRt: seq[seq[nat]] -> seq[seq[nat]] +DEF mapRt(M) == + IF M <>? THEN <> + ELSE rt(ft(M)) :: mapRt(rt(M)) + FI + + +-- Aufgabe 3.3 ---------------------------------------------------------------- + +-- Produkt zweier Matrizen: C = A x B +-- A und B müssen verkettet sein, +-- d.h. Anzahl der Spalten von A = Anzahl der Zeilen von B +FUN matMatProd : seq[seq[nat]] ** seq[seq[nat]] -> seq[seq[nat]] + +/* +-- nicht optimierte Version mit zweimaliger Transposition +DEF matMatProd(M1,M2) == + transp(matMatProdHelp(M1,transp(M2))) +*/ + +-- optimierte Version mit einmaliger Transposition +DEF matMatProd(M1,M2) == + matMatProdHelp(transp(M2),M1) + +-- Pseudo-Produkt zweier Matrizen: +-- Argumente sind A und B, berechnet wird (A x Bt)t, d.h. B x At +-- (t = Transposition) +-- A und Bt müssen verkettet sein +FUN matMatProdHelp : seq[seq[nat]] ** seq[seq[nat]] -> seq[seq[nat]] +DEF matMatProdHelp(M1,M2) == + IF M2 <>? THEN <> + ELSE matVecProd(M1,ft(M2)) :: matMatProdHelp(M1,rt(M2)) + FI + +-- ---------------------------------------------------------------------------- diff --git a/Blatt04/Blatt4.sign b/Blatt04/Blatt4.sign new file mode 100644 index 0000000..7628d97 --- /dev/null +++ b/Blatt04/Blatt4.sign @@ -0,0 +1,72 @@ +SIGNATURE Blatt4 + +IMPORT Nat ONLY nat + Seq[nat] ONLY seq + Seq[seq[nat]] ONLY seq + + +-- Design-Hinweis: +-- Normalerweise ist es nicht besonders sinnvoll, unzusammenhängende +-- Funktionen in einer Struktur anzusammeln. Der Einfachheit halber +-- verzichten wir jedoch darauf, das Aufgabenblatt in mehrere Strukturen +-- aufzuteilen. + + +-- Aufgabe 1 ------------------------------------------------------------------ + +-- Aufgabe 1.1 ---------------------------------------------------------------- + +-- Zerlegung einer natürlichen Zahl größer 1 in ihre Primfaktoren +FUN primeFactorDecomposition: nat -> seq[nat] + + +-- Aufgabe 1.2 ---------------------------------------------------------------- + +-- Aufteilen einer Sequenz in einen monoton aufsteigenden Präfix und den Rest +FUN ascendingPrefix: seq[nat] -> seq[nat] ** seq[nat] + + +-- Aufgabe 2 ------------------------------------------------------------------ + +-- Aufgabe 2.1 (Tut) ---------------------------------------------------------- + +-- Zerlegung einer Sequenz in monoton aufsteigende Teilsequenzen +FUN ascendingParts: seq[nat] -> seq[seq[nat]] + + +-- Aufgabe 2.2 (Tut) ---------------------------------------------------------- + +-- Potenzmenge einer Menge +FUN powerSet: seq[nat] -> seq[seq[nat]] + + +-- Aufgabe 2.3 ---------------------------------------------------------------- + +-- Permutationen einer Sequenz +FUN perm: seq[nat] -> seq[seq[nat]] + + +-- Aufgabe 3 ------------------------------------------------------------------ + +-- Aufgabe 3.1 (Tut) ---------------------------------------------------------- + +-- Produkt aus Matrix und Vektor +-- Die Anzahl der Spalten von M muß gleich der Anzahl der Elemente (Zeilen) +-- von v sein. +FUN matVecProd: seq[seq[nat]] ** seq[nat] -> seq[nat] + + +-- Aufgabe 3.2 ---------------------------------------------------------------- + +-- Transposition einer Matrix +FUN transp: seq[seq[nat]] -> seq[seq[nat]] + + +-- Aufgabe 3.3 ---------------------------------------------------------------- + +-- Produkt zweier Matrizen: C = A x B +-- A und B müssen verkettet sein, +-- d.h. Anzahl der Spalten von A = Anzahl der Zeilen von B +FUN matMatProd: seq[seq[nat]] ** seq[seq[nat]] -> seq[seq[nat]] + +-- ---------------------------------------------------------------------------- diff --git a/Blatt04/blatt4.lsg.pdf b/Blatt04/blatt4.lsg.pdf new file mode 100644 index 0000000..f32d995 Binary files /dev/null and b/Blatt04/blatt4.lsg.pdf differ diff --git a/Blatt04/blatt4.pdf b/Blatt04/blatt4.pdf new file mode 100644 index 0000000..79dc1e8 Binary files /dev/null and b/Blatt04/blatt4.pdf differ diff --git a/Blatt05/HOF.impl b/Blatt05/HOF.impl new file mode 100644 index 0000000..7b83df9 --- /dev/null +++ b/Blatt05/HOF.impl @@ -0,0 +1,96 @@ +IMPLEMENTATION HOF + +IMPORT Nat COMPLETELY +IMPORT Char COMPLETELY +IMPORT Seq COMPLETELY +IMPORT SeqMap COMPLETELY +IMPORT SeqFilter COMPLETELY +IMPORT Compose ONLY o + +/* Aufgabe 1.1 */ + +DEF composeApply(f, g, x) == f(g(x)) + +/* Aufgabe 1.2 */ + +DEF flip == \\ f. \\ x, y. f(y, x) + +/* Aufgabe 1.3 */ + +DEF twice(f) == f o f +-- oder auch +--DEF twice == \\ f. \\ x. (f(f(x))) + +/* Aufgabe 3.1 */ + +DEF curry == \\ f. \\ x. \\ y. f(x, y) + +/* Aufgabe 3.2 */ + +DEF uncurry == \\ f. \\ x, y. f(x)(y) + +/* Aufgabe 3.3 */ + +DEF myAdd == \\ x, y. x + y + +DEF myAddCurry == curry(myAdd) + +DEF plusFive == myAddCurry(5) + +/* Aufgabe 4.1 */ + +DEF myMap(f)(s) == + IF <>?(s) THEN <> + ELSE f(ft(s)) :: myMap(f)(rt(s)) + FI + +DEF myFilter(p)(s) == + IF <>?(s) THEN <> + OTHERWISE + IF p(ft(s)) THEN ft(s) :: myFilter(p)(rt(s)) + ELSE myFilter(p)(rt(s)) + FI + +DEF quicksort(<>) == <> +DEF quicksort(a :: R) == + LET + smaller == filter(\\ x. x < a)(R) + greatereq == filter(\\ x. x >= a)(R) + IN + quicksort(smaller) ++ %(a) ++ quicksort(greatereq) + +DEF toUpper(s) == map(upper)(s) + +/* Aufgabe 4.2 */ + +DEF addFive(s) == map(plusFive)(s) + +DEF toEven(s) == + map(\\ x. IF odd?(x) THEN x + 1 ELSE x FI)(s) + +DEF splitOddEven(s) == + (filter(odd?)(s), filter(even?)(s)) + +DEF raiseEvenBy10(s) == + LET (_, evens) == splitOddEven(s) IN + map(myAddCurry(10))(evens) + +DEF countEven(s) == + #(filter(even?)(s)) + +/* Aufgabe 4.3 */ + +DEF filteredMap(p, f)(s) == + IF <>?(s) THEN <> + OTHERWISE + IF p(ft(s)) THEN f(ft(s)) :: filteredMap(p, f)(rt(s)) + ELSE ft(s) :: filteredMap(p, f)(rt(s)) + FI + +-- oder + +-- DEF filteredMap(p, f)(s) == +-- map(\\x. IF p(x) THEN f(x) ELSE x FI)(s) + + +DEF raise(p, n, s) == filteredMap(p, myAddCurry(n))(s) diff --git a/Blatt05/HOF.sign b/Blatt05/HOF.sign new file mode 100644 index 0000000..0b4874a --- /dev/null +++ b/Blatt05/HOF.sign @@ -0,0 +1,58 @@ +SIGNATURE HOF + +IMPORT Nat ONLY nat +IMPORT Char ONLY char +IMPORT Seq[nat] ONLY seq[nat] +IMPORT Seq[char] ONLY seq[char] + +/* Aufgabe 1.1 */ + +FUN composeApply: (nat -> nat) ** (nat -> nat) ** nat -> nat + +/* Aufgabe 1.2 */ + +FUN flip: (nat ** nat -> nat) -> (nat ** nat -> nat) + +/* Aufgabe 1.3 */ + +FUN twice: (nat -> nat) -> (nat -> nat) + +/* Aufgabe 3.1 */ + +FUN curry: (nat ** nat -> nat) -> nat -> nat -> nat + +/* Aufgabe 3.2 */ + +FUN uncurry: (nat -> nat -> nat) -> nat ** nat -> nat + +/* Aufgabe 3.3 */ + +FUN myAdd: nat ** nat -> nat + +FUN myAddCurry: nat -> nat -> nat + +FUN plusFive: nat -> nat + +/* Aufgabe 4.1 */ + +FUN myMap: (nat -> nat) -> seq[nat] -> seq[nat] + +FUN myFilter: (nat -> bool) -> seq[nat] -> seq[nat] + +FUN quicksort: seq[nat] -> seq[nat] + +FUN toUpper: seq[char] -> seq[char] + +/* Aufgabe 4.2 */ + +FUN addFive: seq[nat] -> seq[nat] +FUN toEven: seq[nat] -> seq[nat] +FUN splitOddEven: seq[nat] -> seq[nat] ** seq[nat] +FUN raiseEvenBy10: seq[nat] -> seq[nat] +FUN countEven: seq[nat] -> nat + +/* Aufgabe 4.3 */ + +FUN filteredMap: (nat -> bool) ** (nat -> nat) -> seq[nat] -> seq[nat] + +FUN raise: (nat -> bool) ** nat ** seq[nat] -> seq[nat] diff --git a/Blatt05/MathHOF.impl b/Blatt05/MathHOF.impl new file mode 100644 index 0000000..2d35026 --- /dev/null +++ b/Blatt05/MathHOF.impl @@ -0,0 +1,11 @@ +IMPLEMENTATION MathHOF + +IMPORT Real COMPLETELY + +DEF shiftX == \\f,x,deltaX. f(x-deltaX) + +DEF mirrorY == \\f,x. 0-f(x) + +DEF myCos == \\x. shiftX(sin,x,0-pi/2) + +DEF myCot == \\x. myCos(x)/sin(x) diff --git a/Blatt05/MathHOF.impl.txt b/Blatt05/MathHOF.impl.txt new file mode 100644 index 0000000..219ecfd --- /dev/null +++ b/Blatt05/MathHOF.impl.txt @@ -0,0 +1,15 @@ +IMPLEMENTATION MathHOF + +IMPORT Real COMPLETELY + +/* Aufgabe 1.4 */ + +-- Die Funktion shiftX verschiebt die Funktion h entlang der x-Achse um deltaX. +DEF shiftX(deltaX)(f)(x) == f(x-deltaX) +-- Die Funktion mirrorY spiegelt die Funktion h an der y-Achse. +DEF mirrorY(f)(x) == f(-(x)) +-- Die Funktion myCos soll die Kosinus-Funktion berechnen. +DEF myCos == shiftX(-(pi/("2"!)))(sin) +-- Die Funktion myCot soll die Kotangens-Funktion berechnen. +DEF myCot == mirrorY(shiftX(-(pi/("2"!)))(tan)) +-- DEF myCot == shiftX(-(pi/("2"!)))(mirrorY(tan)) diff --git a/Blatt05/MathHOF.sign b/Blatt05/MathHOF.sign new file mode 100644 index 0000000..cf8dc12 --- /dev/null +++ b/Blatt05/MathHOF.sign @@ -0,0 +1,8 @@ +SIGNATURE MathHOF + +IMPORT Real ONLY real + +FUN shiftX : (real->real)**real**real->real +FUN mirrorY : (real->real)**real->real +FUN myCos : real->real +FUN myCot : real->real diff --git a/Blatt05/MathHOF.sign.txt b/Blatt05/MathHOF.sign.txt new file mode 100644 index 0000000..49735a4 --- /dev/null +++ b/Blatt05/MathHOF.sign.txt @@ -0,0 +1,10 @@ +SIGNATURE MathHOF + +IMPORT Real ONLY real + +/* Aufgabe 1.4 */ + +FUN shiftX : real -> (real-> real) -> (real->real) +FUN mirrorY: (real -> real)-> (real->real) +FUN myCos : real -> real +FUN myCot : real -> real diff --git a/Blatt05/blatt5.impl b/Blatt05/blatt5.impl new file mode 100644 index 0000000..ebc61b1 --- /dev/null +++ b/Blatt05/blatt5.impl @@ -0,0 +1,103 @@ +IMPLEMENTATION blatt5 + +IMPORT Nat COMPLETELY +IMPORT Seq COMPLETELY +IMPORT Char COMPLETELY + +FUN composeApply : (nat->nat)**(nat->nat)**nat->nat +DEF composeApply == \\f,g,n. f(g(n)) + +-- flip(funktion,wert1,wert2) +FUN flip : (nat**nat->nat)**nat**nat->nat +DEF flip(f,x,y) == f(y,x) + +-- twice(funktion,wert) +FUN twice : (nat->nat)**nat->nat +DEF twice == \\f,n. f(f(n)) + +-- Lösung für Aufgabe: 2.3. : Variante 6 funktioniert! + +-- curry(funktion(,))(wert1)(wert2) +FUN curry : (nat**nat->nat)->nat->nat->nat +DEF curry(f)(x)(y) == f(x,y) + +-- uncurry(funktion()(),wert1,wert2) +FUN uncurry : (nat->nat->nat)**nat**nat->nat +DEF uncurry(f,x,y) == f(x)(y) + +FUN myAdd : nat**nat->nat +-- DEF myAdd == \\x,y. x+y +DEF myAdd(x,y) == x+y + +FUN myAddCurry : nat->nat->nat +DEF myAddCurry(x)(y) == curry(myAdd)(x)(y) + +FUN plusFive : nat->nat +DEF plusFive(x) == myAddCurry(x)(5) + +-- myMap(funktion)(sequenz) +FUN myMap : (nat->nat)->seq[nat]->seq[nat] +DEF myMap(_)(<>) == <> +DEF myMap(f)(a::s) == f(a)::myMap(f)(s) + +-- myFilter(prädikat)(sequenz) +FUN myFilter : (nat->bool)->seq[nat]->seq[nat] +DEF myFilter(_)(<>) == <> +DEF myFilter(p)(a::s) == IF p(a) THEN a::myFilter(p)(s) + ELSE myFilter(p)(s) + FI + +FUN quickSort : seq[nat]->seq[nat] +DEF quickSort(<>) == <> +DEF quickSort(a::R) == LET sm == myFilter(\\x. xa)(R) + IN quickSort(sm) ++ %(a) ++ me ++ quickSort(la) + +FUN quickSort2 : seq[nat]->seq[nat] +DEF quickSort2(<>) == <> +DEF quickSort2(a::R) == LET sm == myFilter(\\x. x=a)(R) + IN quickSort2(sm) ++ %(a) ++ quickSort2(la) + +FUN toUpper : seq[char]->seq[char] +DEF toUpper(<>) == <> +DEF toUpper(a::R) == upper(a)::toUpper(R) + +FUN addFive : seq[nat]->seq[nat] +DEF addFive == \\s. myMap(plusFive)(s) + +FUN toEvenhelper : nat->nat +DEF toEvenhelper == \\x. IF x%2=0 THEN x + ELSE x+1 + FI + +FUN toEven : seq[nat]->seq[nat] +DEF toEven == \\s. myMap(toEvenhelper)(s) + +FUN toEven2 : seq[nat]->seq[nat] +DEF toEven2 == \\s. myMap(\\x. x*2)(s) + +FUN splitOddEven : seq[nat]->seq[nat]**seq[nat] +DEF splitOddEven == \\s. (myFilter(\\x. x%2|=0)(s),myFilter(\\x. x%2=0)(s)) + +FUN raiseEvenBy10 : seq[nat]->seq[nat] +DEF raiseEvenBy10 == \\s. LET (od,ev) == splitOddEven(s) + IN myMap(\\x. x+10)(ev) + +FUN countEven : seq[nat]->nat +DEF countEven(<>) == 0 +DEF countEven(a::R) == IF mod(a,2)=0 THEN 1+countEven(R) + ELSE countEven(R) + FI + +-- filteredMap(funktion)(prädikat)(sequenz) +FUN filteredMap : (nat->nat)->(nat->bool)->seq[nat]->seq[nat] +DEF filteredMap(_)(_)(<>) == <> +DEF filteredMap(f)(p)(a::s) == IF p(a) THEN f(a)::filteredMap(f)(p)(s) + ELSE a::filteredMap(f)(p)(s) + FI + +-- raise(prädikat)(wert)(sequenz) +FUN raise : (nat->bool)->nat->seq[nat]->seq[nat] +DEF raise == \\p. \\x. \\s. filteredMap(myAddCurry(x))(p)(s) \ No newline at end of file diff --git a/Blatt05/blatt5.lsg.pdf b/Blatt05/blatt5.lsg.pdf new file mode 100644 index 0000000..17f7d43 Binary files /dev/null and b/Blatt05/blatt5.lsg.pdf differ diff --git a/Blatt05/blatt5.pdf b/Blatt05/blatt5.pdf new file mode 100644 index 0000000..fac5247 Binary files /dev/null and b/Blatt05/blatt5.pdf differ diff --git a/Blatt05/blatt5.sign b/Blatt05/blatt5.sign new file mode 100644 index 0000000..309a9f6 --- /dev/null +++ b/Blatt05/blatt5.sign @@ -0,0 +1,8 @@ +SIGNATURE blatt5 + +IMPORT Nat ONLY nat +IMPORT Char ONLY char +IMPORT Seq[nat] ONLY seq[nat] +IMPORT Seq[char] ONLY seq[char] + + diff --git a/Blatt06/ListFunc.impl b/Blatt06/ListFunc.impl new file mode 100644 index 0000000..e844de9 --- /dev/null +++ b/Blatt06/ListFunc.impl @@ -0,0 +1,30 @@ +IMPLEMENTATION ListFunc + +IMPORT Seq COMPLETELY +IMPORT Nat COMPLETELY + +FUN myReduce : (nat**nat->nat)**nat->seq[nat]->nat +DEF myReduce == \\f,e. \\s. IF <>?(s) THEN e + ELSE f(ft(s),myReduce(f,e)(rt(s))) + FI + +FUN myZip : (nat**nat->nat)->seq[nat]**seq[nat]->seq[nat] +DEF myZip == \\f. \\s1,s2. IF <>?(s1) or <>?(s2) THEN <> + ELSE f(ft(s1),ft(s2))::myZip(f)(rt(s1),rt(s2)) + FI + +FUN myFold : (nat**nat->nat)**nat->seq[nat]->nat +DEF myFold == \\f,e. \\s. IF <>?(s) THEN e + ELSE myFold(f,f(e,ft(s)))(rt(s)) + FI + +FUN newfD : seq[nat]->nat +DEF newfD == \\s. myFold(-,2*ft(s))(s) + +FUN testfunc : nat**nat**nat->nat +DEF testfunc == \\a,b,c. a+b-c + +FUN zip3 : (nat**nat**nat->nat)->seq[nat]**seq[nat]**seq[nat]->seq[nat] +DEF zip3 == \\f. \\s1,s2,s3. IF <>?(s1) or (<>?(s2) or <>?(s3)) THEN <> + ELSE f(ft(s1),ft(s2),ft(s3))::zip3(f)(rt(s1),rt(s2),rt(s3)) + FI diff --git a/Blatt06/ListFunc.sign b/Blatt06/ListFunc.sign new file mode 100644 index 0000000..ed04177 --- /dev/null +++ b/Blatt06/ListFunc.sign @@ -0,0 +1,5 @@ +SIGNATURE ListFunc + +IMPORT Seq COMPLETELY +IMPORT Nat COMPLETELY + diff --git a/Blatt06/Person.impl b/Blatt06/Person.impl new file mode 100644 index 0000000..1f2a580 --- /dev/null +++ b/Blatt06/Person.impl @@ -0,0 +1,40 @@ +IMPLEMENTATION Person + +IMPORT Nat COMPLETELY +IMPORT Denotation COMPLETELY + +DATA date == date(day : nat, + month : nat, + year : nat) + +DATA person == person(name : denotation, + surname : denotation, + birthdate : date) + +/* Aufg. 2.3. Induzierte Signatur: + + K: FUN person : denotation**denotation**date -> person + D: FUN person? : person -> bool + S: FUN name surname : person -> denotation + FUN birthdate : person -> date + +*/ + +FUN earlier? : date**date -> bool +DEF earlier?(date(a,b,c),date(d,e,f)) == IF c bool +DEF older?(person(_,_,a),person(_,_,b)) == IF earlier?(b,a) THEN true ELSE false FI + +FUN birthday : person -> nat**nat +DEF birthday(person(_,_,date(a,b,_))) == (a,b) + +FUN sameName? : person**person -> bool +DEF sameName?(person(_,a,_),person(_,b,_)) == IF a=b THEN true ELSE false FI + diff --git a/Blatt06/Person.sign b/Blatt06/Person.sign new file mode 100644 index 0000000..3533ef8 --- /dev/null +++ b/Blatt06/Person.sign @@ -0,0 +1,14 @@ +SIGNATURE Person + +IMPORT Nat ONLY nat + +TYPE date == date(day : nat, + month : nat, + year : nat) + +TYPE person == person(name : denotation, + surname : denotation, + birthdate : date) + + + diff --git a/Blatt06/SafeNat.impl b/Blatt06/SafeNat.impl new file mode 100644 index 0000000..d50554f --- /dev/null +++ b/Blatt06/SafeNat.impl @@ -0,0 +1,55 @@ +IMPLEMENTATION SafeNat + +IMPORT Nat COMPLETELY +IMPORT NatConv COMPLETELY +IMPORT Denotation ONLY ++ +IMPORT Seq COMPLETELY +IMPORT SeqMap COMPLETELY + +DATA safeNat == ok (value : nat) + error (message : denotation) + +DEF `(ok(val)) == "ok(" ++ `(val) ++ ")" +DEF `(error(msg)) == "error(\"" ++ msg ++ "\")" + +FUN safePred : safeNat -> safeNat +DEF safePred(error(_)) == error("keine Zahl!") +DEF safePred(ok(n)) == IF n=0 THEN error("null hat keinen...") + ELSE ok(pred(n)) + FI +-- DEF safePred(ok(0)) == error("blabla") +-- DEF safePred(succ(n)) == ok(n) +-- oder aber DEF safePred == safeLift(pred,succ?,"Fehler!") + +FUN safeSucc : safeNat -> safeNat +DEF safeSucc(error(_)) == error("blabla") +DEF safeSucc(ok(n)) == ok(succ(n)) +-- DEF safeSucc == safeLift(succ, \\n. true, "") + +FUN safeLift : (nat->nat)**(nat->bool)**denotation->safeNat->safeNat +DEF safeLift(_,_,_)(error(msg)) == error(msg) +DEF safeLift(f,p,d)(ok(n)) == IF p(n) THEN ok(f(n)) ELSE error(d) FI + +FUN safeLift2 : (nat**nat->nat)**(nat**nat->bool)**denotation->safeNat**safeNat->safeNat +DEF safeLift2(_,_,_)(error(msg),_) == error(msg) +DEF safeLift2(_,_,_)(_,error(msg)) == error(msg) +DEF safeLift2(_,_,_)(error(msg1),error(msg2)) == error(msg1 ++ msg2) +DEF safeLift2(f,p,d)(ok(n1),ok(n2)) == IF p(n1,n2) THEN ok(f(n1,n2)) ELSE error(d) FI + +FUN safeAdd : safeNat**safeNat -> safeNat +DEF safeAdd == \\x,y. safeLift2(+,\\a,b. true,"")(x,y) + +FUN safeSub : safeNat**safeNat -> safeNat +DEF safeSub == \\x,y. safeLift2(-,\\a,b. a>=b,"Geht nicht!")(x,y) + +FUN safeMult : safeNat**safeNat -> safeNat +DEF safeMult == \\x,y. safeLift2(*,\\a,b. true,"")(x,y) + +FUN safeDiv : safeNat**safeNat -> safeNat +DEF safeDiv == \\x,y. safeLift2(/,\\a,b. b>0,"Div durch 0 nicht erklaert!")(x,y) + +FUN safeMap : (nat->nat)**(nat->bool)**denotation->seq[safeNat]->seq[safeNat] +DEF safeMap(_,_,_)(<>) == <> +DEF safeMap(a,b,c)(error(msg)::s) == error(msg)::safeMap(a,b,c)(s) +DEF safeMap(f,p,m)(ok(a)::s) == IF p(a) THEN ok(f(a))::safeMap(f,p,m)(s) ELSE error(m)::safeMap(f,p,m)(s) FI + diff --git a/Blatt06/SafeNat.sign b/Blatt06/SafeNat.sign new file mode 100644 index 0000000..90f6053 --- /dev/null +++ b/Blatt06/SafeNat.sign @@ -0,0 +1,11 @@ +SIGNATURE SafeNat + +IMPORT Nat ONLY nat +IMPORT Seq[safeNat] ONLY seq +IMPORT Seq[nat] ONLY seq + +TYPE safeNat == ok (value : nat) + error (message : denotation) + +FUN ` : safeNat -> denotation + diff --git a/Blatt06/blatt6.lsg.pdf b/Blatt06/blatt6.lsg.pdf new file mode 100644 index 0000000..3455e6f Binary files /dev/null and b/Blatt06/blatt6.lsg.pdf differ diff --git a/Blatt06/blatt6.pdf b/Blatt06/blatt6.pdf new file mode 100644 index 0000000..dddf8d2 Binary files /dev/null and b/Blatt06/blatt6.pdf differ diff --git a/Blatt06/solution.txt b/Blatt06/solution.txt new file mode 100644 index 0000000..f1b253f --- /dev/null +++ b/Blatt06/solution.txt @@ -0,0 +1,141 @@ +Hallo Elena, + +hier kommen die Lösungen für das fünfte Übungsblatt. +In unserer Gruppe sind folgende Leute: +André (ateichi@cs.tu-berlin.de) +Marisa (marisa@cs.tu-berlin.de) +Florian (cerbff@cs.tu-berlin.de) +und ich (mbirth@cs.tu-berlin.de). + +Und jetzt die Lösungen: + + +1.2.: FUN myFold : (nat**nat->nat)**nat->seq[nat]->nat + DEF myFold == \\f,e. \\s. IF <>?(s) THEN e + ELSE myFold(f,f(e,ft(s)))(rt(s)) + FI + + ListFunc.impl>e myFold(\\\\x,y. x+y,5)(%(1,2,3,4)) + 15 + + + + FUN newfD : seq[nat]->nat + DEF newfD == \\s. myFold(-,2*ft(s))(s) + + ListFunc.impl>e newfD(%(8,3,1)) + 4 + +1.3.: FUN zip3 : (nat**nat**nat->nat)->seq[nat]**seq[nat]**seq[nat]->seq[nat] + DEF zip3 == \\f. \\s1,s2,s3. IF <>?(s1) or (<>?(s2) or <>?(s3)) THEN <> + ELSE f(ft(s1),ft(s2),ft(s3))::zip3(f)(rt(s1),rt(s2),rt(s3)) + FI + + ListFunc.impl>e zip3(\\\\x,y,z. x+y-z)(%(1,2,3),%(4,5,6),%(3,2,1)) + <2,5,8> + + + +2.3.: Konstruktoren: FUN person : denotation**denotation**date -> person + + Diskriminatoren: FUN person? : person -> bool + + Selektoren: FUN name surname : person -> denotation + FUN birthdate : person -> date + + +2.4.: FUN earlier? : date**date -> bool + DEF earlier?(date(a,b,c),date(d,e,f)) == IF ce earlier?(date(1,1,"2001"!),date("31"!,"12"!,"2000"!)) + false + Person.impl>e earlier?(date(1,1,"2001"!),date(2,1,"2001"!)) + true + + + + FUN older? : person**person -> bool + DEF older?(person(_,_,a),person(_,_,b)) == IF earlier?(b,a) THEN true ELSE false FI + + Person.impl>e older?(person("Max","Muster",date(1,1,"1979"!)),person("Mina","Muster",date(1,1,"1982"!))) + false + Person.impl>e older?(person("Max","Muster",date(1,1,"1979"!)),person("Mina","Muster",date(1,1,"1974"!))) + true + + + FUN birthday : person -> nat**nat + DEF birthday(person(_,_,date(a,b,_))) == (a,b) + + Person.impl>e birthday(person("Max","Muster",date("29"!,2,"1979"!))) + (29,2) + + + + FUN sameName? : person**person -> bool + DEF sameName?(person(_,a,_),person(_,b,_)) == IF a=b THEN true ELSE false FI + + Person.impl>e sameName?(person("Max","Muster",date(1,1,1)),person("Mini","Muster",date(1,1,1))) + true + Person.impl>e sameName?(person("Max","Muster",date(1,1,1)),person("Mini","Müller",date(1,1,1))) + false + + +3.1.: Konstruktoren: FUN ok : nat -> safeNat + FUN error : denotation -> safeNat + Diskriminatoren: FUN ok? error? : safeNat -> bool + Selektoren: FUN value : safeNat -> nat + FUN error : safeNat -> denotation + +3.4.: FUN safeLift2 : (nat**nat->nat)**(nat**nat->bool)**denotation->safeNat**safeNat->safeNat + DEF safeLift2(_,_,_)(error(msg),_) == error(msg) + DEF safeLift2(_,_,_)(_,error(msg)) == error(msg) + DEF safeLift2(_,_,_)(error(msg1),error(msg2)) == error(msg1 ++ msg2) + DEF safeLift2(f,p,d)(ok(n1),ok(n2)) == IF p(n1,n2) THEN ok(f(n1,n2)) ELSE error(d) FI + + !!Beispiele siehe safeAdd, safeSub, safeMult, safeDiv!! + +3.5.: FUN safeAdd : safeNat**safeNat -> safeNat + DEF safeAdd == \\x,y. safeLift2(+,\\a,b. true,"")(x,y) + + FUN safeSub : safeNat**safeNat -> safeNat + DEF safeSub == \\x,y. safeLift2(-,\\a,b. a>=b,"Geht nicht!")(x,y) + + FUN safeMult : safeNat**safeNat -> safeNat + DEF safeMult == \\x,y. safeLift2(*,\\a,b. true,"")(x,y) + + FUN safeDiv : safeNat**safeNat -> safeNat + DEF safeDiv == \\x,y. safeLift2(/,\\a,b. b>0,"Div durch 0 nicht erklaert!")(x,y) + + SafeNat.impl>e safeSub(ok(5),ok(4)) + ok(1) + SafeNat.impl>e safeSub(ok(5),ok(6)) + error("Geht nicht!") + SafeNat.impl>e safeDiv(ok(5),ok(2)) + ok(2) + SafeNat.impl>e safeDiv(ok(5),ok(0)) + error("Div durch 0 nicht erklaert!") + +3.6.: FUN safeMap : (nat->nat)**(nat->bool)**denotation->seq[safeNat]->seq[safeNat] + DEF safeMap(_,_,_)(<>) == <> + DEF safeMap(a,b,c)(error(msg)::s) == error(msg)::safeMap(a,b,c)(s) + DEF safeMap(f,p,m)(ok(a)::s) == IF p(a) THEN ok(f(a))::safeMap(f,p,m)(s) ELSE error(m)::safeMap(f,p,m)(s) FI + + SafeNat.impl>e safeMap(\\\\x. x+5,\\\\x. true,"Fehler!")(%(ok(1),ok(2),ok(3))) + + SafeNat.impl>e safeMap(\\\\x. 100 / x,\\\\x. x>0,"Div durch 0")(%(ok(1),ok(2),ok(0))) + + +So, das war's. + +Ich hab darauf verzichtet, die ganzen FUNs in die .sign-Dateien zu schieben, +da ich das so übersichtlicher finde und für unsere Testzwecke das eh +belanglos ist. + +Grüsse, + -mARKUS diff --git a/Blatt07/Environment.impl b/Blatt07/Environment.impl new file mode 100644 index 0000000..7d92d31 --- /dev/null +++ b/Blatt07/Environment.impl @@ -0,0 +1,15 @@ +IMPLEMENTATION Environment + +IMPORT Denotation COMPLETELY +IMPORT SafeNat COMPLETELY +IMPORT Seq COMPLETELY + +DATA binding == binding(key: denotation, value: safeNat) +DATA environment == environment(bindings: seq[binding]) + +DEF emptyenv == environment(<>) + +DEF lookup(environment(<>),_) == error("Nicht gefunden") +DEF lookup(environment(binding(k,v)::S),x) == IF k=x THEN v ELSE lookup(environment(S),x) FI + +DEF bind(environment(S),x,v) == environment(binding(x,v)::S) diff --git a/Blatt07/Environment.sign b/Blatt07/Environment.sign new file mode 100644 index 0000000..cfc5f50 --- /dev/null +++ b/Blatt07/Environment.sign @@ -0,0 +1,23 @@ +SIGNATURE Environment + +IMPORT Denotation COMPLETELY +IMPORT SafeNat COMPLETELY + +TYPE binding == binding(key: denotation, value: safeNat) +TYPE environment == environment(bindings: seq[binding]) + +FUN emptyenv : environment +FUN lookup : environment ** denotation -> safeNat +FUN bind : environment ** denotation ** safeNat -> environment + +FUN testenv : environment +DEF testenv == bind(bind(emptyenv,"test",ok(5)),"test2",ok(2)) + +FUN test1 : safeNat +DEF test1 == lookup(testenv,"test") + +FUN test2 : safeNat +DEF test2 == lookup(testenv,"test2") + +FUN testfail : safeNat +DEF testfail == lookup(testenv, "isnichdrin") diff --git a/Blatt07/Interpreter.impl b/Blatt07/Interpreter.impl new file mode 100644 index 0000000..71aa531 --- /dev/null +++ b/Blatt07/Interpreter.impl @@ -0,0 +1,10 @@ +IMPLEMENTATION Interpreter + +IMPORT SafeNat COMPLETELY +-- IMPORT Expression COMPLETELY +IMPORT Environment COMPLETELY +-- IMPORT Evaluate COMPLETELY + +DATA expr == lamda(parameter: denotation, result: expr) + apply(fun: expr, arg: expr) + diff --git a/Blatt07/Interpreter.sign b/Blatt07/Interpreter.sign new file mode 100644 index 0000000..b573489 --- /dev/null +++ b/Blatt07/Interpreter.sign @@ -0,0 +1,4 @@ +SIGNATURE Interpreter + +IMPORT SafeNat COMPLETELY +IMPORT Environment COMPLETELY diff --git a/Blatt07/SafeNat.impl b/Blatt07/SafeNat.impl new file mode 100644 index 0000000..5546a98 --- /dev/null +++ b/Blatt07/SafeNat.impl @@ -0,0 +1,46 @@ +IMPLEMENTATION SafeNat + +IMPORT Nat COMPLETELY +IMPORT NatConv COMPLETELY +IMPORT Denotation ONLY ++ +IMPORT Seq COMPLETELY +IMPORT SeqMap COMPLETELY + +DATA safeNat == ok (value : nat) + error (message : denotation) + +DEF `(ok(val)) == "ok(" ++ `(val) ++ ")" +DEF `(error(msg)) == "error(\"" ++ msg ++ "\")" + +DEF safePred(error(_)) == error("keine Zahl!") +DEF safePred(ok(n)) == IF n=0 THEN error("null hat keinen...") + ELSE ok(pred(n)) + FI +-- DEF safePred(ok(0)) == error("blabla") +-- DEF safePred(succ(n)) == ok(n) +-- oder aber DEF safePred == safeLift(pred,succ?,"Fehler!") + +DEF safeSucc(error(_)) == error("blabla") +DEF safeSucc(ok(n)) == ok(succ(n)) +-- DEF safeSucc == safeLift(succ, \\n. true, "") + +DEF safeLift(_,_,_)(error(msg)) == error(msg) +DEF safeLift(f,p,d)(ok(n)) == IF p(n) THEN ok(f(n)) ELSE error(d) FI + +DEF safeLift2(_,_,_)(error(msg),_) == error(msg) +DEF safeLift2(_,_,_)(_,error(msg)) == error(msg) +DEF safeLift2(_,_,_)(error(msg1),error(msg2)) == error(msg1 ++ msg2) +DEF safeLift2(f,p,d)(ok(n1),ok(n2)) == IF p(n1,n2) THEN ok(f(n1,n2)) ELSE error(d) FI + +DEF safeAdd == \\x,y. safeLift2(+,\\a,b. true,"")(x,y) + +DEF safeSub == \\x,y. safeLift2(-,\\a,b. a>=b,"Geht nicht!")(x,y) + +DEF safeMult == \\x,y. safeLift2(*,\\a,b. true,"")(x,y) + +DEF safeDiv == \\x,y. safeLift2(/,\\a,b. b>0,"Div durch 0 nicht erklaert!")(x,y) + +DEF safeMap(_,_,_)(<>) == <> +DEF safeMap(a,b,c)(error(msg)::s) == error(msg)::safeMap(a,b,c)(s) +DEF safeMap(f,p,m)(ok(a)::s) == IF p(a) THEN ok(f(a))::safeMap(f,p,m)(s) ELSE error(m)::safeMap(f,p,m)(s) FI + diff --git a/Blatt07/SafeNat.sign b/Blatt07/SafeNat.sign new file mode 100644 index 0000000..03d0284 --- /dev/null +++ b/Blatt07/SafeNat.sign @@ -0,0 +1,20 @@ +SIGNATURE SafeNat + +IMPORT Nat ONLY nat +IMPORT Seq[safeNat] ONLY seq +IMPORT Seq[nat] ONLY seq + +TYPE safeNat == ok (value : nat) + error (message : denotation) + +FUN ` : safeNat -> denotation +FUN safePred : safeNat -> safeNat +FUN safeSucc : safeNat -> safeNat +FUN safeLift : (nat->nat)**(nat->bool)**denotation->safeNat->safeNat +FUN safeLift2 : (nat**nat->nat)**(nat**nat->bool)**denotation->safeNat**safeNat->safeNat +FUN safeAdd : safeNat**safeNat -> safeNat +FUN safeSub : safeNat**safeNat -> safeNat +FUN safeMult : safeNat**safeNat -> safeNat +FUN safeDiv : safeNat**safeNat -> safeNat +FUN safeMap : (nat->nat)**(nat->bool)**denotation->seq[safeNat]->seq[safeNat] + diff --git a/Blatt07/blatt7.impl b/Blatt07/blatt7.impl new file mode 100644 index 0000000..701c702 --- /dev/null +++ b/Blatt07/blatt7.impl @@ -0,0 +1,35 @@ +IMPLEMENTATION blatt7 + +IMPORT Nat COMPLETELY +IMPORT Seq COMPLETELY +IMPORT Denotation COMPLETELY + +FUN f: nat -> (nat -> nat) -> nat ** nat -> nat +DEF f == \\a. \\b. \\c,d. ( g(2+f1(a)(b(e),c)) + WHERE + (e,g) == f2(c,d,b) ) + +FUN perms: seq[nat] -> seq[seq[nat]] +DEF perms(S) == IF <>?(S) THEN <> :: <> ELSE fold(\\a1,b1. fold(\\a2,b2. (b1::b2)::a2,a1)(perms(S-b1)),<>)(S) FI + +FUN perms2: seq[nat] -> seq[seq[nat]] +DEF perms2(S) == + IF <>?(S) THEN + empty1 :: empty2 + WHERE + empty1 == <> + empty2 == <> + ELSE + result + WHERE + result == foldf1(S) + foldf1 == fold(f1,empty3) + empty3 == <> + f1 == \\a1,b1. ( foldf2(perms2(S-b1)) + WHERE + foldf2 == fold(f2,a1) + f2 == \\a2,b2. (b1 cons1 b2) cons2 a2 ) + cons1 == \\b1,b2. b1::b2 + cons2 == \\b1_cons1_b2,a2. b1_cons1_b2::a2 + FI + diff --git a/Blatt07/blatt7.pdf b/Blatt07/blatt7.pdf new file mode 100644 index 0000000..e7c57b4 Binary files /dev/null and b/Blatt07/blatt7.pdf differ diff --git a/Blatt07/blatt7.sign b/Blatt07/blatt7.sign new file mode 100644 index 0000000..5418681 --- /dev/null +++ b/Blatt07/blatt7.sign @@ -0,0 +1,6 @@ +SIGNATURE blatt7 + +IMPORT Nat COMPLETELY +IMPORT Seq COMPLETELY +IMPORT Denotation COMPLETELY + diff --git a/Blatt08/blatt8.lsg.pdf b/Blatt08/blatt8.lsg.pdf new file mode 100644 index 0000000..a232ecd Binary files /dev/null and b/Blatt08/blatt8.lsg.pdf differ diff --git a/Blatt08/blatt8.pdf b/Blatt08/blatt8.pdf new file mode 100644 index 0000000..663eaa7 Binary files /dev/null and b/Blatt08/blatt8.pdf differ diff --git a/Blatt09b/blatt9.lsg.pdf b/Blatt09b/blatt9.lsg.pdf new file mode 100644 index 0000000..11ad36e Binary files /dev/null and b/Blatt09b/blatt9.lsg.pdf differ diff --git a/Blatt09b/blatt9b.pdf b/Blatt09b/blatt9b.pdf new file mode 100644 index 0000000..8b20c6e Binary files /dev/null and b/Blatt09b/blatt9b.pdf differ diff --git a/Blatt10/blatt10.lsg.pdf b/Blatt10/blatt10.lsg.pdf new file mode 100644 index 0000000..6f6fd13 Binary files /dev/null and b/Blatt10/blatt10.lsg.pdf differ diff --git a/Blatt10/blatt10.pdf b/Blatt10/blatt10.pdf new file mode 100644 index 0000000..f4f78ac Binary files /dev/null and b/Blatt10/blatt10.pdf differ diff --git a/Blatt11/blatt11.lsg.pdf b/Blatt11/blatt11.lsg.pdf new file mode 100644 index 0000000..22f2d28 Binary files /dev/null and b/Blatt11/blatt11.lsg.pdf differ diff --git a/Blatt11/blatt11.pdf b/Blatt11/blatt11.pdf new file mode 100644 index 0000000..95d32c5 Binary files /dev/null and b/Blatt11/blatt11.pdf differ diff --git a/README.md b/README.md new file mode 100644 index 0000000..2183f81 --- /dev/null +++ b/README.md @@ -0,0 +1,4 @@ +OPAL - OPtimized Applicative Language +===================================== + +( See http://en.wikipedia.org/wiki/Opal_(programming_language) ) diff --git a/RealFun.impl b/RealFun.impl new file mode 100644 index 0000000..8a6b372 --- /dev/null +++ b/RealFun.impl @@ -0,0 +1,53 @@ +IMPLEMENTATION RealFun + +-- Einzeilige Kommentare werden mit einem doppelten Minus eingeleitet. + +/* +Kommentare +ueber mehrere Zeilen +sehen so aus. +*/ + +/* Fuer alle Berechnungen brauchen wir hier die Struktur Real, + die Fliesskommazahlen und ihre Operationen, wie z.B. *, +, + und Konstanten, wie z.B. pi, bereitstellt. + + Erlaeuterungen zur Basisstruktur Real findet Ihr unter + http://uebb.cs.tu-berlin.de/infadm/opal/doc/kommentierteLib/doc/shortbib_toc.html + Dort koennt Ihr weitere, fuer die Loesung der Aufgaben evtl. + notwendige Funktionen heraussuchen. +*/ + +IMPORT Real COMPLETELY + +/* + Gegeben ist hier ein Beispiel einer Funktionsdefinition. + Diese Implementierung einer Funktion kann zwar von + oasys uebersetzt werden, sie ist aber *nicht* korrekt. + Daher soll sie von Euch korrigiert werden. + + Die Quadratfunktion: +*/ + +DEF square(X) == X * X + +DEF cube(X) == X * square(X) + +DEF reciprocal(X) == 1/X + +DEF ld(X) == ln(X)/ln(2) + +DEF circ(D) == pi/4 * square(D) + +-- Argument D: Durchmesser + +DEF vol(D,H) == circ(D) * H + +-- Argument D: Durchmesser +-- Argument H: Hoehe des Zylinders + +DEF len(X,Y,Z) == sqrt(square(X) + square(Y) + square(Z)) + +-- Argumente X,Y,Z sind die Koordinaten des Vektors + + diff --git a/RealFun.sign b/RealFun.sign new file mode 100644 index 0000000..4cdc022 --- /dev/null +++ b/RealFun.sign @@ -0,0 +1,25 @@ +SIGNATURE RealFun + +/* Diese Datei enthaelt die Schnittstelle (den Signaturteil + der Struktur). Die eigentliche Implementierung muss von + Euch in der Datei RealFun.impl vorgenommen werden. */ + +IMPORT Real ONLY real + +/* Die Sorte real wird aus der Struktur Real importiert. + Sie wird gebraucht, um die Definitions- und Wertebereiche + der folgenden Funktionen angeben zu koennen. */ + +FUN square : real -> real + +FUN cube : real -> real + +FUN reciprocal : real -> real + +FUN ld : real -> real + +FUN circ : real -> real + +FUN vol : real ** real -> real + +FUN len : real ** real ** real -> real