]> git.example.dev Git - research-obsidian.git/commitdiff
functional programming lectures, AD notes
author2weiEmu <saalbach.robert@outlook.de>
Wed, 26 Feb 2025 10:27:52 +0000 (11:27 +0100)
committer2weiEmu <saalbach.robert@outlook.de>
Wed, 26 Feb 2025 10:27:52 +0000 (11:27 +0100)
Algorithm Design/Definitions.md [new file with mode: 0644]
Algorithm Design/Greedy.md [new file with mode: 0644]
Algorithm Design/Resources.md [new file with mode: 0644]
Functional Programming/Functional Programming Introduction.md
Functional Programming/Lecture 2.md

diff --git a/Algorithm Design/Definitions.md b/Algorithm Design/Definitions.md
new file mode 100644 (file)
index 0000000..2a70f10
--- /dev/null
@@ -0,0 +1,16 @@
+# DAG
+> A _DAG_ is a directed graph that contains no directed cycles.
+>      If something is a _DAG_ then it has a node with no incoming edges.
+# Topological Ordering
+> A _topological ordering_ of a directed graph $G = (V,E)$ is an ordering of its nodes as $v_1, v_2, ..., v_n$ so that for every edge $(v_i, v_j)$ we have $i < j$.
+       What does this mean, simply? 
+       The graph is ordered in such a way that you disconnect the graph and never leave an edge hanging, you resolve all edges first and only if there is no in-bound edges, you can get rid of that vertex.
+
+# Strong vs. Weak Induction
+> You refer to all previous steps, instead of just the previous single one. The first case is strong induction, the second is weak.
+
+# Lemma
+A preliminary proposition useful for proving later propositions.
+
+# Corollary
+An afterthought, a proposition that follows in just a few logical steps from a theorem.
\ No newline at end of file
diff --git a/Algorithm Design/Greedy.md b/Algorithm Design/Greedy.md
new file mode 100644 (file)
index 0000000..767ca36
--- /dev/null
@@ -0,0 +1,40 @@
+What is the correct formulation of an upper bound on the runtime of algorithm?
+> The runtime is $O(n)$.
+
+## Selecting Breakpoints for Delft -> Copenhagen
+(Remember this example?)
+
+### Proof by Induction: Greedy stays ahead
+- With equal number of stops, greedy is at least as close to the goal as the optimal solution.
+- Greedy thus is optimal
+
+### Example by Induction:
+Let $0 = g_1 < g_2 < ... < g_p = L$ denote the campsites (distance) chosen by greedy. 
+Let $0 = f_1 < f_2 < ... < f_p = L$ denote the campsites in an optimal solution.
+
+Lemma: $\forall r: f_r \leq g_r$ with g for Greedy campsites and f for some optimal sol.
+       in words?
+       the lemma is, in this case you want to show that furthest campsite the optimal solution is at, is at least as far as greedy, or further away (from the destination.)
+
+Base Case (r=1):
+- When r=1 $g_1$ is as far away as possible, i.e. $f_1 \leq g_1 \leq C$
+       (the first step is the farthest we can go)
+Induction Hypothesis (IH):
+- Suppose that for some k it holds that $f_k \leq g_k$.
+       (so, let's say that at some point its true that it does better)
+Induction Step:
+- to prove: for k+1 it holds that $f_{k+1} \leq g_{k+1}$
+       (prove that it also does better next time then)
+- We know that $f_k \leq g_k$ by IH
+- Greedy selects the next farthest campsite possible ($g_{k+1}\leq g_k + C$ to be as far as possible from $g_k$)
+- Campsite $f_{k+1}$ cannot be further than $f_k + C$, and this is def. at most $g_k+C$ because of the IH. So $f_{k+1}\leq g_{k+1}$.
+
+This does not, necessarily prove that it selects fewer campsites. this we have to prove again. Proof by contradiction.
+
+### Example by Contradiction (fewer sites):
+- let k be the number of campsites selected by greedy, and m the number of sites by an optimal solution.
+- Suppose greedy is not optimal. So k > m, and thus $g_m < f_m$,
+       - this would mean that the optimal solution would be ahead of greedy at that point - which we proved doesn't happen.
+- However, $f_m \leq g_m$ with the lemma from the [[Greedy#Example by Induction|previous proof]]. 
+- Contradiction with $g_m < f_m$. So greedy must be optimal.
+
diff --git a/Algorithm Design/Resources.md b/Algorithm Design/Resources.md
new file mode 100644 (file)
index 0000000..83cb8f7
--- /dev/null
@@ -0,0 +1,8 @@
+Guide on proof:
+https://brightspace.tudelft.nl/d2l/le/content/680727/viewContent/3806787/View
+
+Guide on writing inductions:
+https://brightspace.tudelft.nl/d2l/le/content/680727/viewContent/3806789/View
+
+How to use invariants:
+https://brightspace.tudelft.nl/d2l/le/content/680727/viewContent/3806788/View
\ No newline at end of file
index 752f3049a765133fe6f41f8520f3154ca3701c23..dd012eeb16266fafa50577ff463d9acd08a70676 100644 (file)
@@ -108,4 +108,5 @@ Why Num a? because technically, this is the broadest category that these fit in,
 _this may have changed apparently idfk_
 
 
-`type String = [Char]`
\ No newline at end of file
+`type String = [Char]`
+
index cc38144b745bdf2f3c4cd5f05d230ced1b95e6f0..49db9db9b2007cc2f10924d1384fe4c62f33bdc6 100644 (file)
@@ -152,3 +152,169 @@ you cannot use the 'num' type on its own, its a constraint not a type itself, so
 
 There is the `Eq` class.
 `Ord` class, things that can be ordered. Subclass of `Eq`
+
+
+# Lecture 3 is here now
+Type alias
+```haskell
+type Coordinate = (Int, Int)
+```
+you can assign meaning to types
+
+there is also paramterised types
+
+```haskell
+type Pair a = (a, a)
+type Assoc k v = [(k, v)]
+
+-- an alias for a function type
+type Transformation = Coordinate -> Coordinate
+```
+
+Type aliases _cannot_ be recursive
+
+## Algebraic Datatypes (ADT)
+```haskell
+data Answer = Yes | No | DontKnow
+       deriving (Show)
+
+answers :: [Answer]
+answers = [Yes, No, DontKnow]
+
+flip :: Answer -> Answer
+flip Yes      = No
+flip No       = Yes
+flip DontKnow = DontKnow
+```
+
+`Show` is a [[Lecture 2#Type Classes|type class]]
+
+
+```haskell
+test x y = case compare x y of 
+       LT -> y - x
+       EQ -> 1
+       GT -> x - y
+```
+How to use the compare and case functions
+
+
+```haskell
+compare :: Ord a => a -> a -> Ordering
+```
+
+```haskell
+data Shape = Circle Double | Rect Double Double
+square :: Double -> Shape
+square x = Rect x x
+
+area :: Shape -> Double
+area (Circle r) = pi * r * r
+area (Rect l h) = l * h
+```
+
+## Constructors as Functions
+Each constructor defines a function into the datatype
+
+## `newtype` declarations
+A `newtype` declaration is a (more efficient) `data` declaration with exactly one constructor taking exactly one argument:
+```haskell
+newtype EuroPrice = EuroCents Integer
+newtype DollarPrice = DollarCents Integer
+```
+
+(these are really new types, and not just sugar / aliasses, so they will throw, for example type errors when they are passed incorrectly for example)
+
+type checker will check 'newtype' as different, but in the final compiled code they will be the same. Treated differently by the typechecker, but not by the compiler
+
+## Record Syntax
+haskell provides an alternative record syntax to define constructors with arguments:
+```haskell
+data Shape
+       = Circle { radius :: Double }
+       | Rect { width :: Double, height :: Double }
+```
+this will just also define the functions 'radius', 'width', 'height' and stuff
+but it will define it for shape, so you can encounter a runtime error when you, for example call "radius" on a Rect.
+
+```haskell
+radius :: Shape -> Double -- one of the functions that gets automatically defined.
+```
+
+```haskell
+data Circle2 = Circle2 Double
+data Circle2 = Circle2 { radius :: Double }
+```
+
+the thing on the left, is the name of the type, on the right is the name of the constructor
+
+## The Haskell Type `Maybe`
+the type `Maybe a` represents an optional value of type a:
+```haskell
+data Maybe a = Nothing | Just a
+```
+
+`Maybe` is often used to represent functions that can fail
+
+```haskell
+safeDiv :: Int -> Int -> Maybe Int
+safeDiv x y 
+       | y == 0 = Nothing
+       | otherwise = Just (x `div` y)
+```
+
+## A Safer `head` Function 
+```haskell
+safeHead :: [a] -> Maybe a
+safeHead [] = Nothing
+safeHead (x:xs) = Just x
+```
+
+### Non-Empty Lists
+```haskell
+data NonEmpty a = a :| [a]
+
+toList :: NonEmpty a -> [a]
+toList (x :| xs) = x : xs
+```
+here `:|` is the constructor, and was written in-between 'infix'
+
+### The `Either` Type
+The `Either` type repsent a disjooint union of a and b: each element is either Left x for x:: a or Right y for y :: b.
+
+```haskell
+data Either a b = Left a | Right b
+```
+
+Convention. Right is often used to represent a successful operation, while Left is often used to represent an error
+
+## Counting Functions
+How many possible functions of type `Bool -> Answer` are there?
+9.
+why?
+```haskell
+\b -> if b then Yes else Yes
+\b -> if b then No else Yes
+\b -> if b then Unknown else Yes
+\b -> if b then Yes else No
+\b -> if b then No else No
+\b -> if b then Unknown else No
+\b -> if b then Yes else Unknown
+\b -> if b then No else Unknown
+\b -> if b then Unknown else Unknown
+```
+
+## What's Algebraic about ADTs?
+An algebraic datatype is a type that is formed from other types using sums and porducts:
+- The product of a and b is the tuple type (a,b)
+- The sum of a and b is the disjoint union of type `Either a b`
+
+## Recursive Data
+We can define a type `Nat` represents natural numbers (inefficiently) as Zero, Suc Zero, Suc (Suc Zero), ...:
+```haskell
+daata Nat = Zero | Suc Nat
+int2nat :: Int -> Nat
+int2nat 0 = Zero
+int2nat n
+       | n > 0 = Suc (int2nat (n-1))
+```