👋 Hello, I'm Damien

This is a loosely collected set of notes on computer science and related/applicable fields of study.

They are typically quite raw and only for my own personal use, except for posts in the editorials section, which are intended as blog posts for public consumption.

Software engineering is about division of labor

Between users and machines...

Between clients and servers...

Between different programmers...

Between different modules...

Tension lies between notions of abstraction and composition

Abstraction (which embodies division)

Composition (which embodies harmony)

PL theory is "advancing linguistic solutions to the contradiction between abstraction and composition" - Reynolds, 1983.

This is a beautiful quote from a presentation by Jon Sterling.

I am fascinated by PL theory, type theory, and the idea of the computational trilogy, and this informs how I think about my work as a professional software developer.

My goal is to pull useful abstractions from the fields of logic, philosophy, ethics, and artificial intelligence (at least in my particular niche as a research engineer) and make them available both to my colleagues at work as well as to interested others in the open source and general public.

Hopefully, the decision to publish both my raw and refined thoughts via this mdbook will help motivate me to keep articulating, editing, and learning indefinitely.

This section pertains to hobby or independent, open-source work.

Computational Type Theory

A lecture series given by Bob Harper at OPLSS 2018

Part One

Lecture 1

Type theory from a computational perspective

References

Martin-Löf, Constructive Mathematics and Computer Programming
Constable et al., NuPRL System & Semantics

The plan is to develop type theory starting with computation, and developing a theory of truth based on proofs. The connection with formalisms (e.g. theories of proofs, formal derivation, etc.) comes later.

The idea is to emphasize not just playing the Coq/Agda/Lean video game!

Start with a programming language

The language has a deterministic semantics via a transition system.

We have forms of expression called

$E$

and two judgement forms called

$E v a l$

$E \mapsto E^{'}$

These mean that $E$ is fully evaluated, and that we have performed one simplification of $E$ , respectively.

We have a derived notion

$E ⇓ E_{\circ}$

which we can understand by way of a mapping

$E \mapsto^{⋆} E_{\circ} v a l$

As an example expression

$i f (E_{1}; E_{2}) (E)$

Operational semantics for binary decision diagrams

$\frac{E ⟼ E ^{'}}{i f ( E _{1} ; E _{2} ) ( E ) ⟼ i f ( E _{1} ; E _{2} ) ( E ^{'} )}$

$i f ( E _{1} ; E _{2} ) ( t r u e ) ⟼ E _{1}$

$i f ( E _{1} ; E _{2} ) ( f a l se ) ⟼ E _{2}$

Principle: types are specifications of program behavior

Judgements are expressions of knowledge, in the intuitionistic sense (Brouwer), based on the premise that mathematics is a human activity, thus finite, and that the only way to constrain facts about infinite infinities (Gödel, Russell?) is via algorithms.

E.g. there is no way to convey infinitely many utterly disconnected facts about $N a t$ other than to have a uniformity expressed as an algorithm. We agree on such uniformity solely because of the fundamental faculties of the human mind w.r.t. computation.

$M$ and $A$ here are programs, and are behavioral, not structural. ${A t y p e M \in A$

For example:

$i f (17;_) (t r u e) \in N a t$

Why? Because the simplification step entails $17 \in N a t$ .

Further:

$i f (N a t; B oo l) (M)$

is a type precisely when:

$M \in B oo l$

This applies to type expressions as well, e.g.

$i f (17; t r u e) (M) \in i f (N a t; B oo l) (M)$

This helps explain why a deterministic operational semantics is required, because it is the same $M$ in the simplification step. Types/specifications are programs.

Type-indexed families of types a.k.a. dependent types

We can make a judgement that:

$se q (n) t y p e$

precisely when

$n \in N a t$

And that:

$n : N a t ≫ se q t y p e$

That is, a family of types is indexed by a type. Another way to phrase it, which emphasizes the indexing of a sequence by $n \in N a t$ is:

$\forall n \exists se q (n)$

where:

$se q (n) ≐ [0.. n - 1]$

In NuPRL notation:

$f \in n : N a t \to S e q (n)$

This is sometimes represented in the literature as:

$Π n : N a t S e q (n)$

Functionality

Families (of types, of elements) must respect equality of indices. So what is equality?

Trivially:

$se q (2 + 2)$

is "the same as"

$se q (4)$

or in other words

$se q (i f (17; 18) (M))$

is "the same as"

$i f (se q (17); se q (18)) (M)$

which can be clarified with a slight change in notation, substituting $a : B oo l$ for $M$

As a type structure gets richer, when two things are equal is a property of the type they inhabit, and it can be arbitrarily complicated. The situation about what is true has a much higher -- in fact -- unbounded quantifier of complexity, whereas the question of what is written down in any formalism is always relentlessly recursively enumerable. This means that formalisms can never approach equality-based truth! This standpoint is validated by Gödel's theorem.

Indeed, the entire endeavour of higher-dimensional type theory arises from investigating when two types are the same.

Judgements

When $A$ is a type:

$A ≐ A^{'}$

specifies an exact equality of types.

When $M \in A$ :

$M ≐ M^{'} \in A$

specifies an exact equality of elements.

Thus, equal indices deterministically produce equal results (this is also why a deterministic operational semantics is a necessity). A term for this is equisatisfaction.

A simple example is the following:

$2 ≐ 4 \in N a t$

cannot be true...

However:

$2 ≐ 4 \in N a t /2 (e v e n s)$

is true!. It always depends on type inhabitants.

This is in contrast to the older tradition in formalized type theory of axioms as being somehow type-independent. By the principle of propositions-as-types, we now know this is is a logical fallacy.

To make the notation a little clearer, from here on we will try to write:

$M ≐ M^{'} \in A$

as:

$M ≐_{A} M^{'}$

A computational semantics

$A ≐ A^{'}$

means that

$A ≐ A^{'} ⎩ ⎨ ⎧ A ⇓ A_{\circ} A^{'} ⇓ A_{\circ}^{'} A_{\circ} ≐_{\circ} A_{\circ}^{'}$

$A_{\circ}$ and $A_{\circ}^{'}$ are equal type-values, or what Martin-Löf called canonical types.

$M ≐_{A} M^{'}$ is thus a program which evaluates to equal type-values.

A few core ideas

Given that

$A ⇓ A_{\circ} A_{\circ} ≐_{\circ} A_{\circ}$

we can say

$⎩ ⎨ ⎧ M ⇓ M_{\circ} M^{'} ⇓ M_{\circ}^{'} M_{\circ} ≐_{\circ} M_{\circ}^{'} \in A_{\circ}$

Thus

$a : A ≫ B ≐ B^{'}$

means

$i f (M ≐ M^{'} \in A) t h e n (B [M / a] ≐ B^{'} [M^{'} / a])$

This induces a certain implication about type indexing, called functionality:

Check that $⎩ ⎨ ⎧ a : A ≫ B where B M^{'} implies B [M / a] ≐ B ≐ M^{'} \in A ≐ B [M^{'} / a]$

A final example in the general case:

$a : A ≫ N ≐ N^{'}$

means

$i f M ≐ M^{'} \in A t h e n (N [M / a] ≐ N^{'} [M^{'} a] \in B [M / a])$

assuming

$a ≫ B ≐ B$

A specific example by deriving the Boolean type

$B oo l ≐_{\circ} B oo l$

i.e. $B oo l$ names a type-value (hence the $_\circ$ ).

What type does it name? The membership relation for canonical elements is

$M_{\circ} ≐ M_{\circ}^{'} \in_{\circ} B oo l$ is the strongest relation $R$ (though some literature calls this least, the extremal nature is what is important)

such that

$R \subseteq (E x p \times E x p) {(t r u e ≐_{\circ} t r u e \in B oo l) i . e . t r u e \in_{\circ} B oo l (f a l se ≐_{\circ} f a l se \in B oo l) i . e . f a l se \in_{\circ} B oo l$

The extremal clause is that

The stated conditions hold.
Nothing else!

We can now make proposition/fact/claim, and prove it. We'll use this format from here onward.

Fact

$M \in B oo l$

and

$A t y p e$

and

$M_{1} \in A$

and

$M_{2} \in A$

then

$i f (M_{1}; M_{2}) (M) \in A$

Proof

$_\in B oo l$ is given by a universal property, the least (or most) containing ${t r u e \in B oo l f a l se \in B oo l$
Fix some type $A$ , $M_{1} \in A$ , $M_{2} \in A$ .
If $M \in B oo l$ then $i f (M_{1}; M_{2}) (M) \in A$
Thus, $M \in B oo l$ means $M ⇓ M_{\circ}$ and either ${M_{0} M_{0} ≐ t r u e ≐ f a l se$
It suffices to show that ${i f (M_{1}; M_{2}) (t r u e) \in A i f (M_{1}; M_{2}) (f a l se) \in A$
$i f$ evaluates its principal arguments (via a transition step). Typing is closed under "head-expansion" or alternatively "reverse execution".
$■$

Part Two

Lecture 2

Where we are so far

A type system consists of $A ≐ A$ with $A$ called a $t y p e$ $i ff$ $A ≐ A$ .

$M ≐ M$ with $M \in A$ $i ff$ $M ≐ M \in A$ .

The expression above is both symmetric and transitive, that is

If $A ≐ A^{'}$ and $M ≐ M^{'} \in A$ then $M ≐ M^{'} \in A$

Hypotheticals express functionality:

$a : A ≫ B t y p e$

This means $B$ is a family of types that depends functionally on $a : A$ .

$M ≐ M^{'} \in A$

implies

$B [M / a] ≐ B [M^{'} / a]$

$a : A ≫ N \in B$

means that $B$ is a family of elements; A family of elements is a mapping.

The expression

$M ≐ M^{'} \in A$

implies

$N [M / a] ≐ N [M^{'} / a] \in B [M / a] ≐ B [M^{'} / a]$

Similarly for $B ≐ B^{'}$ , $N ≐ N^{'} \in B$

All of the above constitutes a type system defined in terms of evaluation (hence computational) using the language of constructive mathematics.

Now we can start to write down fragments of our own type theories.

There exists a type system containing a type `bool`

Presuming

$B oo l ≐ B oo l$

The expression

$M ≐ M^{'} \in B oo l$

is true $i ff$ either

$(M ^{'} ⇓ t r u e M ⇓ t r u e)$

$(M ^{'} ⇓ f a l se M ⇓ f a l se)$

Fact

$a : B oo l ≫ B t y p e$

and

$M_{1} \in B [t r u e / a]$

and

$M_{2} \in B [f a l se / a]$

and

$M \in B oo l$

then

$i f (M_{1}; M_{2}) (M) \in B [M / a]$

Proof

Either $M ⇓ t r u e$
- $∴ M ≐ t r u e \in B oo l$ by head expansion (reverse execution)
or $M ⇓ f a l se$
- $∴ M ≐ f a l se \in B oo l$ by head expansion (reverse execution)
$■$

An example

Given $M_{1} \in B [t r u e / a]$

$i f (M_{1}; M_{2}) (M) ≐ i f (M_{1}; M_{2}) (t r u e) ≐ M_{1} \in B [t r u e / a] ≐ B [M / a]$ ✅

This can be generalized by Shannon expansion.

If $a : B oo l ≫ P \in B$ then $P [M / a] ≐ i f (P [t r u e / a]; P [f a l se / a]) (M)$

Which can be seen as a "pivot on $M$ ". Binary decision diagrams are created by choosing pivots in a way that minimizes the size of conditionals.

The given facts look like definitions in a formal type system, and this is intentional.
Semantics define what is true, and formalisms that follow are a pale approximation which are useful for impl.
These "little lemmas" are the method of logical relations; type-indexed information determines what equality means.

There exists a type system containing a type `Nat`

$N a t ≐ N a t$

$M ≐ M^{'} \in N a t$

is the extremal (strongest/least) statement s.t.

Either $(M ^{'} ⇓ 0 M ⇓ 0)$
Or $(M ^{'} ⇓ s u cc ( N ^{'} ) M ⇓ s u cc ( N ))$ $N ≐ N^{'} \in N a t$
The extremal clause provides a morally-equivalent notion of an induction principle.

Given some assumptions

$0 v a l$

$s u cc ( M ) v a l$

We can define the Y-combinator

$f i x (a . s u cc (a)) \mapsto ω : = s u cc (f i x a . s u cc (a))$

$ω \in C o N a t$

is thus the greatest solution to the specification

$ω \in / N a t$

We may now define a recursor $R$ .

$R : = rec (M_{\circ}; a, b . M_{1}) (M) \mapsto rec (M_{\circ}; a, b . M_{1}) (M^{'})$

$M \mapsto M^{'}$

and

$R (0) \mapsto M_{\circ}$

and

$R (s u cc (m)) \mapsto M_{1} [M, R (M) / a, b]$

Fact

$a : N a t ≫ B t y p e$ $M_{\circ} \in B [0/ a]$ $a : N a t, b : B ≫ M_{1} \in B [s u cc (a) / a]$

If $M \in N a t$ then $R (M) \in B [M / a]$

Proof

Case for $0$ :

$M ⇓ 0$
$M ≐ 0 \in N a t$
$M_{\circ} \in B [0/ a] ≐ B [m / a]$
$R (M) ≐ R (0) ≐ M_{\circ}$
$R (M) \in B [M / a]$
$■$

Case for $s u cc (N)$

$M ⇓ s u cc (N)$
Given an inductive hypothesis $R (N) \in B [N / a]$ ... (the proof is unfinished)

These ( $B oo l$ , $N a t$ ) are representative examples of inductive types (least extremal clauses that satisfy some conditions). They are not representative examples of coinductive types (most extremal clauses that imply/are consistent with some conditions).

There exists a type system containing a type `Prod`

$(A_{1} \times A_{2}) ≐ (A_{1}^{'} \times A_{2}^{'})$

$i ff$

$A_{1} ≐ A_{1}^{'}$

and

$A_{2} ≐ A_{2}^{'}$

and

$M ≐ M^{'} \in (A_{1} \times A_{2})$

$i ff$

${M ⇓ ⟨ M_{1}, M_{2} ⟩ M^{'} ⇓ ⟨ M_{1}^{'}, M_{2}^{'} ⟩$

where

$M_{n} ≐ M_{n}^{'} \in A_{n}$

that is, that the values for each $M_{n}$ are evaluated under the conditions in $A_{n}$

Fact

If $M \in A_{1} \times A_{2}$ then $M .0 \in A_{1}$ and $M .1 \in A_{2}$ (one could sub other notation here, e.g. fst, etc.)

where

$\frac{M \mapsto M ^{'}}{M . i _{1} \mapsto M . i _{2}}$

and

$( M _{1} , M _{2} ) . i \mapsto M _{i}$

and $(i = f s t, s n d)$

A note about logical relations as a tactic: membership in product types is defined in terms of equality in each of the component types. Constituent types are, in a sense, already given, and then we speak about the composite types.

Going further...

If $M_{1} \in A_{1}$ , then $(M_{1}, M_{2}) .1 ≐ M_{1} \in A_{1}$ , which has no requirement on $M_{2}$ .

Recall that by head-expansion (a.k.a reverse-execution) $(M_{1}, M_{2}) .1 \mapsto M_{1}$ .

This may seem like a "technical anomaly", but is an important insight into how computational type theory relies on specifications as opposed to a grammar for writing down well-formed things according to syntactic rules that impose additional requirements beyond those described by this fact. Formalisms are about obeying protocols.

Completing the proof of fact w.r.t. Prod from the assumptions (in similar vein to the earlier examples) is left as an exercise.

There exists a type system containing a type `Fn`

$A_{1} \to A_{2} ≐ A_{1}^{'} \to A_{2}^{'}$

$i ff$

$A_{1} ≐ A_{1}^{'}$

and

$A_{2} ≐ A_{2}^{'}$

and

$M ≐ M^{'} \in A_{1} \to A_{2}$

$i ff$

$M ⇓ λa . M_{2}$

and

$M^{'} ⇓ λa . M_{2}^{'}$

where

$a : A ≫ M_{2} ≐ M_2 \in A_{2}$

Given some assumptions

$λa . M v a l$

$\frac{M \mapsto M ^{'}}{a p ( M , M 1 ) \mapsto a p ( M ^{'} , M _{1} )}$

$a p ( λa . M _{2} , M 1 ) \mapsto M _{2} [ M _{1} / a ]$

The latter is a kind of $β$ -reduction, or at least a well-specified reduction strategy.

Fact

If $M \in A_{1} \to A_{2}$ and $M_{1} \in A_{1}$ then $a p (M, M_{1}) \in A_{2}$ .

We can translate this into a usual type-theoretic notation like so

$\frac{Γ ⊢ M : A _{1} \to A _{2} Γ ⊢ M _{1} : A _{1}}{Γ ⊢ a p ( M , M _{1} ) : A _{2}}$

and the inductive definition is the "protocol" or "syntax" of the aforementioned fact.

Observe: what is the quantifier complexity of $M ≐ M^{'} \in N a t \to N a t$ ?

In an informal sense, one can say

$\forall M_{1} ≐ M_{1}^{'} \in N a t \exists P_{1} ≐ P_{1}^{'} \in N a t$

such that

$a p (M, M_{1}) ≐ a p (M^{'}, M_{1}^{'}) \in N a t$

This is the reason that starting with the formal syntax is inadequate, because an induction rule like

$Γ ⊢ M \equiv M ^{'} : N a t \to N a t$

is a derivation tree that results in a quantifier complexity of "there exists something". But $\forall \exists$ cannot be captured by $\exists$ alone!

Fact

$M, M^{'} \in A_{1} \to A_{2}$

and

$a : A_{1} ≫ a p (M, a) ≐ a p (M^{'}, a)$

then

$M ≐ M^{'} \in A_{1} \to A_{2}$

One may call this "function extensionality"

Completing the proof of facts w.r.t. Fn from the assumptions (in similar vein to the earlier examples) is left as an exercise.

This is profound: One cannot axiomatize equality in $N a t \to N a t$ by a deeper understanding of Gödel's theorem.

There exists a type system containing a type `Dependent Prod`

$a : A_{1} \times A_{2} ≐ a : A_{1}^{'} \times A_{2}^{'}$

$i ff$

$A_{1} ≐ A_{1}^{'}$

$a : A_{1} ≫ A_{2} ≐ A_{2}^{'}$

$M ≐ M^{'} \in (A_{1} \times A_{2})$

$i ff$ ${M ⇓ ⟨ M_{1}, M_{2} ⟩ M^{'} ⇓ ⟨ M_{1}^{'}, M_{2}^{'} ⟩$

where

$M_{1} ≐ M_{1}^{'} \in A_{1}$

and, different from Prod,

$M_{2} ≐ M_{2}^{'} \in A_{2} [M_{1} / a] ≐ A_{2} [M_{1}^{'} / a]$

which encodes the dependency between $A_{1}$ and $A_{2}$ .

There exists a type system containing a type `Dependent Fn`

$a : A_{1} \to A_{2} ≐ a : A_{1}^{'} \to A_{2}^{'}$

$i ff$

$A_{1} ≐ A_{1}^{'} - a : A_{1} ≫ A_{2} ≐ A_{2}^{'}$

From the definition, it's easy enough to look back at the definitions / initial transitions for Fn and subsitute the following, as we did for Prod

$a : A_{1} ≫ M_{2} ≐ M_{2}^{'} \in A_{2} (a)$

The meaning of the change is as follows:

$M_{1} ≐ M_{1}^{'} \in A_{1}$

then

$M_{2} [M_{1} / a] ≐ M_{2} [M_{1}^{'} / a] \in A_{2} [M_{1} / a] ≐ A_{2} [M_{1}^{'} / a]$

Fact

If $M \in a : A_{1} \times A_{2}$ then $M .0 \in A_{1}$ and $M .1 \in A_{2} [M .0/ a]$
If $M \in a : A_{1} \to A_{2}$ and $M_{1} \in A_{1}$ then $a p (M, M_{1}) \in A_{2} [M_{1} / a]$

Completing the proof of fact w.r.t. Dependent Fn from the assumptions (in similar vein to the earlier examples) is left as an exercise.

In summary, so far

This is a development of a simple, inherently computational dependent type system

$τ : = B oo l ∣ N a t ∣ a_{1} : A_{1} \times A_{2} ∣ a_{1} : A_{1} \to A_{2}$

which can be used to prove an earlier claim

$i f (17; t r u e) (M) \in i f (N a t, B oo l) (M)$

Part Three

Lecture 3

Formalisms

Formal type theory is inductively defined by derivation rules.

We want to express some statements regarding what is called "definitional equality".

$Γ ⊢ A : T y p e$

$Γ ⊢ M : A$

$Γ ⊢ A \equiv A^{'}$

$Γ ⊢ M \equiv M^{'} : A$

One can write down axioms of the typical form:

$Γ x : A , Γ ^{'} ⊢ x : A$

$\frac{Γ ⊢ M : A Γ ⊢ A \equiv A ^{'}}{Γ ⊢ M : A ^{'}}$

$\frac{Γ ⊢ A _{1} Γ ⊢ A _{2}}{Γ ⊢ A _{1} \times A _{2}}$

$\frac{Γ ⊢ M _{1} : A _{1} Γ M _{2} : A _{2}}{Γ ⊢ ( M _{1} , M _{2} ) : A _{1} \times A _{2}}$

$\frac{Γ ⊢ M : A _{1} \times A _{2}}{Γ ⊢ M . i : A _{i}}$

where $i$ is one of the projections of $\times$ .

$\frac{Γ ⊢ M _{1} : A _{1} Γ ⊢ M _{2} : A _{2}}{Γ ⊢ ( M _{1} , M _{2} ) . i \equiv M _{i} : A _{i}}$

$\frac{Γ ⊢ M : A _{1} \times A _{2}}{Γ ⊢ ( M _{1} , M _{2} ) \equiv M : A _{1} \times A _{2}}$

Formal logic statements and their corresponding types

$⊤^{⋆} ⟹ 1$

called unit

$⊥^{⋆} ⟹ 0$

called void

$(Φ_{1} \land Φ_{2})^{⋆} ⟹ Φ_{1}^{⋆} \times Φ_{2}^{⋆}$

called product

$(Φ_{1} \lor Φ_{2})^{⋆} ⟹ Φ_{1}^{⋆} + Φ_{2}^{⋆}$

called sum

$(Φ_{1} \supset Φ_{2})^{⋆} ⟹ Φ_{1}^{⋆} \to Φ_{2}^{⋆}$

called function

$(\forall a : A . Φ_{a})^{⋆} ⟹ a : A \to Φ_{a}^{⋆}$

called function[a]

$(\exists a : A . Φ_{a})^{⋆} ⟹ a : A \times Φ_{a}^{⋆}$

called product[a]

Part Four

Lecture 4

Part Five

Lecture 5

Algebraic Effects and Handlers

Andrej Bauer

Basics

Take the operation symbol for $pl u s$ :

$pl u s : 1 \times Z^{2} \to Z$

3 + (4 + 5)

plus(b:2 if b = 0 then 3
         else plus(c:2 if c = 0 then 4
                       else 5))

$Op : A^{n} \to A$

where $n$ is the arity, or number of distinct effects

$Op : B \times A^{n} \to A$

where $B$ is the parameter type, a monad

$Op : B \times A^{C} \to A$

where $C$ is an unbounded type; a delimited continuation

Sources

Non-markup code which is adjacent to this repo can be found here: https://github.com/damienstanton/notes

Code will generally, as in the notes, be written in Rust, Swift, Haskell, or Agda.

This section pertains to coursework notes in the Master's in Computer Science (MSCS) program at CU Boulder.

CSCA 5414: Greedy Algorithms

Rod cutting is shown as a canonical example of using DP in a recursive and then memoized setting (a third example recovering the data from the table is elided for brevity).

#![allow(unused)]
fn main() {
// Naive attempt to implement the recurrence (see dp_rodcutting.ipynb)
fn max_revenue_recursive(len: i32, sizes: &Vec<i32>, prices: &Vec<f64>) -> i32 {
  if len == 0 {
    return 0;
  }
  if len < 0 {
    return -100_000_000;
  }
  let k = sizes.len();
  assert_eq!(prices.len(), k);
  let mut option_values = vec![];
  for i in 0..k {
    option_values.push(prices[i] + max_revenue_recursive(
      len-sizes[i], sizes, prices
    ) as f64);
  }
  option_values.push(0.);
  option_values.into_iter().reduce(f64::max).unwrap() as i32
}

#[test]
fn examples() {
    let sizes = vec![1, 3, 5, 10, 30, 50, 75];
    let prices = vec![0.1, 0.2, 0.4, 0.9, 3.1, 5.1, 8.2];
    assert_eq!(3.0, max_revenue_recursive(30, &sizes, &prices).round());
    assert_eq!(5.0, max_revenue_recursive(50, &sizes, &prices).round());
    assert_eq!(33.0, max_revenue_recursive(300, &sizes, &prices).round());
}
}

Assumptions

$k \geq 1$
L is a positive usize
sizes and prices will always have the same length

Fining an optimal substructure

Given some length $L$ , we say

A cut of $L_{i}$ pays $P_{i}$ revenue.
Optimally cut remaining $L - L_{i}$

Example recurrence relations

$maxRevenue (L) = max ⎩ ⎨ ⎧ 0 p_{1} + maxRevenue (L - l_{1}) p_{2} + maxRevenue (L - l_{2}) ⋮ p_{k} + maxRevenue (L - l_{k}) \leftarrow Waste the current length of rod without cutting it \leftarrow Choosing Option 1: yields revenue p_{1} and cuts off l_{1} \leftarrow Choosing Option 2: yields revenue p_{2} and cuts off l_{2} ⋮ \leftarrow Choosing Option k: yields revenue p_{k} and cuts off l_{k}$

Example base cases

$maxRevenue (L) = 0$ whenever $L = 0$ . If no rod to cut then nothing to do.
$maxRevenue (L) = - \infty$ whenever $L < 0$ . If there is negative rod to cut, we will "punish" the cutter infinitely.

#![allow(unused)]
fn main() {
// Memoized version
fn max_revenue_memoize(len: i32, sizes: &Vec<i32>, prices: &Vec<f64>) -> f64 {
    let n = len as usize;
    let k = sizes.len();
    assert_eq!(prices.len(), k);

    let mut table = vec![0.; n + 1];
    let mut vals = vec![];

    for i in 1..n + 1 {
        for j in 0..k {
            let i = i as i32;
            if i - sizes[j] >= 0 {
                let idx = (i - sizes[j]) as usize;
                vals.push(prices[j] + table[idx] as f64);
                vals.push(0.);
                table[i as usize] = vals
                  .clone()
                  .into_iter()
                  .reduce(f64::max)
                  .unwrap()
            }
        }
    }
    table[n]
}

#[test]
fn examples() {
    let sizes = vec![1, 3, 5, 10, 30, 50, 75];
    let prices = vec![0.1, 0.2, 0.4, 0.9, 3.1, 5.1, 8.2];
    assert_eq!(3.0, max_revenue_memoize(30, &sizes, &prices).round());
    assert_eq!(5.0, max_revenue_memoize(50, &sizes, &prices).round());
    assert_eq!(33.0, max_revenue_memoize(300, &sizes, &prices).round());
}
}

When no optimal substructure exists

Noting some conditions of the well-known knapsack problem, where $W$ is weight.

$\sum W_{ij} \leq W_{\circ}$

Value: ${\sum V_{ij} i f n < 10 \sum V_{ij} i f n \geq 10$

An alternate example of non-optimal substructure is path-finding, where movement decisions may be disjoint. The sequencing of finding optimal substructures thus becomes the driving factor.

EMEA 5065: The neuroscience of leading high-performance teams

Desires

Finances and work
Relationships
Health
Recreation
Moral, ethical, and spiritual

Greed

Stimulates motivation centers in the brain (more one has, ++ rewards one seeks)
E.g. sharing accumulated wealth with others often leads to greater emotional satisfaction
Brain evolved to anticipate extreme scarcity, we need to actively retrain to anticipate abundance

Two forms of desire

Unconscious drive to survive (bottom-up)
Conscious wanting by optimistic fantasies about the future (top-down) “wishful seeing” <- what we want to tap into in teams. “Breadcrumb” model for long-term driving of goals.

Dopamine control circuit

Manage uncontrolled urges of dopamine desire
Guides “raw energy” towards profitable ends
Abstract concepts and forward-looking strategies
Imagination
Control of world

Desire circuit vs control circuit

Phantoms: things we wish to have
Phantoms: building blocks of imagination, creative thought
Motivation and persistence
- Cost-benefit tradeoffs
- Celebrating small wins
"I don't care anymore; I need to stop for good and call it a day" vs "I'm going to take a short break and regroup by focusing on why achieving this goal matters to me and keep going”

References

Dopaminergic circuitry responds not to reward or pleasure, but to reward prediction error

$R_{actual} - R_{expected}$

Keeping expectations low can maximize the delta between actual and expected rewards
Think about this w.r.t. goal setting, and how to discretize tasks
Anticipation, reward prediciton error, novelty, and curiosity drive motivation
Pain and fear diminish motivation, but drive growth and learning (push through to harder goals)

Barriers to motivation

Physical pain
Unpleasant emotional experiences
Ruminating on unpleasant thoughts

Time boxing is a technique to properly process negative experiences (small mourning) - even 90 seconds.

Distant goals and desires (future oriented)

"Time to hunt vs time to eat"

Switch transition from forward-oriented dopamine (wanting) to present-oriented (H&N) dopamine.
Pursue hard, long-term goals
Dopaminergic personality
- Bored easily
- Enjoys anticipation and planning more than doing
- Easily distracted
- Loves thrill of chase > prize
Dopamine fasting (trendy take on asceticism) has some validity but shouldn't be taken to extremes. Fasting, of any kind, can be addictive.
Ocytocin
- Associated initially with sex & breastfeeding
- Synthesized by the brain when needed, short half-life (~ 3 minutes)
- Ocytocin in analogy to dopamine is not a "trust hormone", but rather anticipation of trustworthiness.

What is engagement?

Activates the prefrontal cortex, provides a sense of empowerment and motivation, activates areas of the brain involved in reflection and introspection, driving fulfillment and satisfaction.

Engagement must utilize the social interfaces wired into the brain
- Reward systems
- Trust systems
  - Sense of autonomy and control over one's work, decision-making
  - Sense of meaning and purpose; serving a larger mission

Social brain and compassion

Insula (sensorimotor processing, sense of self) and anterior cingulate cortex (threat-processing, pain or suffering)
- Helps connect the goal-seeking desires of the prefrontal-cortex with the interroceptive centers (amygdala, limbic areas)
- Drives our ability to feel compassion and guilt

SCARF model

Status
Certainty
Autonomy
Relatedness (ingroup/outgroup)
Fairness

General ideas

Be mindful of instance labels
Find and work with "chemistry creators"

This section stands in the place of a normal blog.

DS Notes

👋 Hello, I'm Damien

Computational Type Theory

Part One

Type theory from a computational perspective

Start with a programming language

Operational semantics for binary decision diagrams

Principle: types are specifications of program behavior

Type-indexed families of types a.k.a. dependent types

Functionality

Judgements

A computational semantics

A few core ideas

A specific example by deriving the Boolean type

Part Two

Where we are so far

There exists a type system containing a type `bool`

There exists a type system containing a type `Nat`

There exists a type system containing a type `Prod`

There exists a type system containing a type `Fn`

There exists a type system containing a type `Dependent Prod`

There exists a type system containing a type `Dependent Fn`

In summary, so far

Part Three

Formalisms

Formal logic statements and their corresponding types

Part Four

Part Five

Algebraic Effects and Handlers

Basics

Sources

CSCA 5414: Greedy Algorithms

Assumptions

Fining an optimal substructure

Example recurrence relations

Example base cases

When no optimal substructure exists

EMEA 5065: The neuroscience of leading high-performance teams

🤷