Add exam notes for db and pp

3 files changed, 224 insertions, 21 deletions

diff --git a/sem7/pp/eksamnen.md b/sem7/pp/eksamnen.md
index 6641d2a..be694ae 100644
--- a/sem7/pp/eksamnen.md
+++ b/sem7/pp/eksamnen.md
@@ -7,6 +7,9 @@
 
 ## Alt Andet
 
+  - "The last condition ..." i logic part 2 1:40. Er det rigtigt?
+  - Er det ikke en fejl i 0:32 i prolog lists videon
+
 # Mixed
 
 *Parameters* is in the declaration, and *arguments* are the things actually passed.
@@ -21,6 +24,19 @@ The arguments are placed in the body according to the parameters.
 
 **Eta** says that functions that just pass arguments to other functions can be substritued by its body.
 
+## Some Haskell Things
+
+```haskell
+-- if
+hej = if (x == 10) then 2 else 3
+
+-- List comprehention
+evens = [i | i <- [0..], i `mod` 2 == 0]
+
+-- Here True and False are *term contructors* and Boolean is a *type constructor*
+data Boolean = True | False
+```
+
 # Scheme lek. 1
 
 Programming paradigm
@@ -184,3 +200,189 @@ Therefore normal order is the post powerful reduction
 
 `(delay expr)` is used to delay the evaluation of `expr`, by returning a promise.
 The value of this can then be extracted with `(force promise)`.
+
+# Haskell lec.5 Lazy Evaluation
+
+Lazy evaluation is the default in haskell.
+Semanticly it is quite simple requiring only a small amount of rules.
+
+There is the beta rewrite rule from before.
+And then there is *application* rule which states that for an application `e1 e2` we only evaluatate `e1`.
+This means that `e2` is newer evaluated before the application is done.
+
+# Haskell lec.7 Type Systems
+
+## Simple Type System
+
+Her har man at expressions kan have simple typer som Int, Bool, eller funktionener og tuples.
+Dette giver nogle forskellige garantier.
+
+Hvis `e` er *wel typed* og `e` reducere til `e'`, så er `e'` også vel typed.
+Dette hedder **subject reduction** og siger noget om *type preservation*.
+
+Den anden er at hvis `e` er *well typed*, så terminere `e`, altså der er en `e'` som er `e` reduceret og `e'` kan ikke reduceres længere.
+Dette er **type safety**.
+
+Disse garantier betyder også at der er mange ting man ikke kan representere.
+For eksempel hvad hvis man gerne vil lave programmer der terminere.
+
+Dette kan man sige fordi det imple type system har *slack*.
+Dette er fordi der er expressions der er safe, men ikke er vel typed.
+For eksempel:
+
+```
+let f = x: x; in (f 0, f True)
+```
+
+Dette giver bare `(0, True)` men det er ikke well typed, fordi der ikke en type for `f`.
+
+## Parametric Polymorhism
+
+Her introducere man
+
+  - **Type variables** som der kan representere hvad som helst.
+  - **Type schemes** som siger noget om free og bound type variables.
+
+Hvis ens type scheme ikke har nogen quantifier for en bestemt type variable, så er den variabel *free*.
+
+Her kan man sige at `Ftv(t)` finder alle frie type variables i typen `t`.
+Her kan man også sige `Ftv(E)` for type environment `E` så er resultatet `Ftv(t)` for alle typer `t` i `E`.
+
+### Specialization
+
+Her snakker man om at et type scheme er en specialization af en type.
+Så man laver en type fra en type scheme.
+
+Så for eksempel er `Int -> Int \leq \forall a. a -> a`.
+
+### Generalization
+
+Her er det det omvendte, med at man laver en type scheme ud fra en type.
+Dette er hvis man har en type har free variable `a`, så kan man lave et scheme der indeholder `\forall a`.
+
+Dette gør man med funktionen `close(E, t)`.
+Denne funktion ville tage og lave quantifiers for alle `Ftv(t) \setminus Ftv(E)`.
+
+### Principle Types
+
+En type `t` er principle for expression `e` og type env `E` hvis enten
+
+  - `t` er typen for `e` i `E`,
+  - eller typen `t1` for `e` i `E` er en specialization af `t`.
+
+Så man kan kalde principle types den mest generelle type.
+
+Her vil vi gerne have et *type inference algorithm* der finder den principielle type for en expression.
+
+### Semantic Regler
+
+Her introducere man nogle regler der sammen med gamle regler kan identificere typer for expressions.
+Dette er `PROJ` som laver specialization, og `GENERALIZATION` som laver generalization.
+
+# Haskell lec.8 More Typing
+
+## Type Classes
+
+With typeclasses, we now say that the quantifiers in a scheme do not say `a can be everything` but `a is part of typeclass \Gamma`.
+We use `\Gamma` for a collection of type classes.
+
+Dette betyder at når man normalt bestemte tyder ud fra et environment der mapper Vars til Types,
+er der nu også en `C` der mapper fra typevariabler til typeclasses.
+
+Okay tror jeg laver de her noter på papir.
+Lidt meget matematik.
+
+# Logic lec.9 Introduction and Datalog
+
+Her skriver jeg igen noter på papir.
+
+# Logic lec.10 Datalog
+
+**Herbrand universe** is the set of constant that appear in the datalog program.
+These are the things which we can talk about.
+
+The **Herbrand base** is then the set of all ground atoms that can be created.
+This is basicly all the things we can say about the **Herbrand universe**, giving a pretty large set.
+
+## Interpretation
+
+An *interpretation* is a set of atoms from the Herbrand universe.
+This could be any subset, and does not have to have to make sense.
+
+We will now talk about how a clause can be true under an interpretation, or how an interpretation models a clause.
+Here facts are easy, as we just check if it is contained in the interpretation.
+A rule is only false if all the facts in the body are true and the head is false, due to the implicative nature of rules.
+
+## Model
+
+We say that an interpretation is a model for a clause, if every ground instance of the clause is true under the interpretation.
+Such an interpretation we denote with M.
+
+We denote the *minimal model* for a program as the smallest possible model for the program.
+This mimimal model can be found as the intersection between all models of the program.
+
+We can find it by starting with the empty interpretation, and then repeatedly extend it will all possible conclusions from the program.
+First facts are added, and then we will start adding conclusions from rules.
+This process will always finish.
+
+## Proof Directed Goal Search
+
+Instead of computing the minimal model, we are only interested in a specific conclusion or query.
+This is done with *goal directed proof search*.
+
+This is done by constructing a proof tree.
+Here we branch the tree every time we have to choose between two clauses.
+
+## Negation in Datalog
+
+In Datalog we can only negate atoms, and not rules.
+Therefore we destinquist negative and positive atoms.
+A negative atom can then only appear in the body of a rule and not the head.
+
+Here we extend the idea of when an atom is in an interpretation, such that `I |= not p(t)` holds if `p(t)` is not in `I`.
+
+In datalog we need to do some stuff for stuff to make sense, as we can create programs with multiple incompatible models:
+
+```prolog
+P(x) :- not Q(x).
+Q(x) :- not P(x).
+```
+
+Therefore we want to disallow circularity, which we do by defining layers.
+We split the program in subprograms, where each subprogram only refers to things from the preveous layer.
+We call this *stratification*.
+
+## Some Words
+
+  - *Model-theoretical* semantics refers to finding a solution with Herbrand universe and base, interpretation and minimal models.
+  - *Fixed-point* semantics is the bottom up approach, where we compute the minimal model.
+  - *Proof-theoretical* semantics is the top down approach, with proof trees.
+
+These can be shown to be equivalent.
+
+The idea of a minimal model does not make much sense with prolog, as the minimal models can be infinite.
+
+# Logic lec.11 Prolog Instead of Datalog
+
+One should remember that prolog uses proof search instead of computing minimal model.
+With proof search and the existence of recursive clauses, the ordering of clauses matters.
+This is because the order of clauses determines the order in which proof search tries things.
+
+## Some Short Prolog Things
+
+```prolog
+% This mimics the idea of haskells composite types.
+nat(zero).
+nat(succ(X)) :- nat(X).
+
+% Some list notation
+% [1,2,3] er det samme som [1 | [2 | [3 | []]]]
+```
+
+The above thing means that the herbrand base is infinite.
+
+## Proof Search
+
+We check each clause in the order in which they appear.
+If the head of a clause matches, we unify it with the body of the clause.
+We then get new goals which we continue with.
diff --git a/sem7/pp/larger.hs b/sem7/pp/larger.hs
index 5618faf..2cf8e57 100644
--- a/sem7/pp/larger.hs
+++ b/sem7/pp/larger.hs
@@ -1,5 +1,26 @@
 import Data.Maybe
 
+-- Fra lec5
+valid :: (Integral a, Ord a) => [(a, b)] -> Bool
+valid = recur empty
+  where recur _ [] = True
+        recur known (pair:rest) =
+          if key `member` known
+          then False
+          else recur (insert key known) rest
+          where key = fst pair
+
+
+-- TODO, case where key is not in is unhandled
+lookup' :: (Integral a, Ord a) => [(a, b)] -> a -> b
+lookup' (pair:rest) key = if (fst pair) == key
+                          then (snd pair)
+                          else lookup' rest key
+
+-- I dont see how findfun and lookup are not the same
+findfun = lookup'
+
+
 data LTree = LLeaf String | LNode LTree LTree
 data LTreeRoot = LTreeRoot LTree Float
 
diff --git a/sem7/pp/lec5.hs b/sem7/pp/lec5.hs
index 3340346..37f6b12 100644
--- a/sem7/pp/lec5.hs
+++ b/sem7/pp/lec5.hs
@@ -39,7 +39,7 @@ ispalindrome x = x == reverse' x
 
 
 -- Okay assuming that a are all integers, i
--- would say that the fype of cfrac :: (Real a, Integral b) -> a -> b -> [b]
+-- would say that the fype of cfrac :: (Real a, Integral b) => a -> b -> [b]
 
 cfrac _ 0 = []
 cfrac x n = let intPart = truncate x in
@@ -69,23 +69,3 @@ flatten' (x:xs) = x ++ flatten' xs
 -- The function type is therefore flatten' :: [[a]] -> [a]
 
 -- When running :t on flatten' we get the same.
-
-
-valid :: (Integral a, Ord a) => [(a, b)] -> Bool
-valid = recur empty
-  where recur _ [] = True
-        recur known (pair:rest) =
-          if key `member` known
-          then False
-          else recur (insert key known) rest
-          where key = fst pair
-
-
--- TODO, case where key is not in is unhandled
-lookup' :: (Integral a, Ord a) => [(a, b)] -> a -> b
-lookup' (pair:rest) key = if (fst pair) == key
-                          then (snd pair)
-                          else lookup' rest key
-
--- I dont see how findfun and lookup are not the same
-findfun = lookup'