From 84ae9c0267a32488d5163e4fec325fb723703090 Mon Sep 17 00:00:00 2001 From: Julian T Date: Tue, 11 Jan 2022 12:01:29 +0100 Subject: Add exam notes for db and pp --- sem7/pp/eksamnen.md | 202 ++++++++++++++++++++++++++++++++++++++++++++++++++++ sem7/pp/larger.hs | 21 ++++++ sem7/pp/lec5.hs | 22 +----- 3 files changed, 224 insertions(+), 21 deletions(-) (limited to 'sem7/pp') 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' -- cgit v1.2.3