recents

src/dependently_typed_languages/coq/program_verification.md

@@ -0,0 +1,9 @@
+# Program Verification
+
+We finished `Imp.v` knowing:
+1. We can write fixpoints (total functions) for `aeval` and `beval`,
+2. However, `ceval` can not be a fixpoint, since 
+there is no way of totally unfolding a while expression.
+3. The solution is to write `ceval` as a relation (not even a function).
+In Coq, this means to make `ceval`'s result a `Prop`, which is allowed
+to not terminate.

src/dependently_typed_languages/front.md

@@ -1 +1,5 @@
 # Dependently_Typed_Languages
+
+The goal is to eventually synthesize all of these languages such that I can present a feature and show its realization in multiple language. But for now, for my own note taking purposes, they would have to be separate.
+
+Reminder: Make a list of capabilities for each language and think critically about what is accomplishable/unaccomplishable in each.

src/dependently_typed_languages/lean/front.md

@@ -1 +1,36 @@
 # Lean
+
+## Dependent Types
+Leans thinks of dependent types as types that depend on parameters (not necessarily values).
+For example, in
+
+```lean
+inductive Vector (α : Type u) : Nat → Type u where
+  | nil  : Vector α 0
+  | cons : (a : α) → {n : Nat} → Vector α n → Vector α (n + 1)
+```
+, `Vector α n` depends on two parameters: the type of the elements in the vector (a type) and the length of the vector (a value).
+
+The Lean books conceptualizes dependent products as dependent functions and adopts
+the "indexed family of types" view of dependent products.
+Dependent functions can be seen as `(a: α) -> β a`. `β` is a family of types over `α`, that is, there is a type `β a` for each value `a: α`. 
+
+Indexed family
+
+This is fundamentally different from type constructors, which have form `(α: Type) -> β α`. With type constructors, values aren't mentioned.
+So "indexed family" is something 
+
+ given `α: Type` and `β: α -> Type`, 
+
+
+For example, consider
+```lean
+def cons (α : Type) (a : α) (as : List α) : List α :=
+  List.cons a as
+```
+
+
+
+
+
+think of β as a family of types over α, that is, a type β a

src/foundations/incompleteness_undecidability_inconsistency/front.md

@@ -1 +1,14 @@
 # Incompleteness_Undecidability_Inconsistency
+
+
+- Why must non-terminating (non-total) functions be rejected in Coq?
+Here is an example showing what would go wrong if Coq allowed non-terminating recursive functions:
+
+```coq
+Fixpoint loop_false (n : nat) : False := loop_false n.
+```
+As a consistent logic, this is not allowed. How would one define the evaluation function for 
+a small imperative language with a `while` construct in Coq, then? One way is to not define 
+a function (which ought to be total) in the first place, but a relation. We define an
+inductive proposition whose return type is `Prop`. The cost of this is that we now need
+to construct a proofs for evaluations.

src/foundations/propositions_as_types/front.md

@@ -1 +1,61 @@
-# Propositions_As_Types
+# Propositions As Types
+
+Curry noticed that every proof in propositional logic corresponded (bidirectionally) to a function (term) in the (simply) typed lambda calculus. For example, consider
+
+```
+λx:a->b. λy:a. x y
+```
+, since this is proper function (term) in the simply typed lambda calculus, it witnesses the truth of some statement in propositional logic, intuitively, we know this is
+```
+(a->b) -> a -> b
+```
+
+A false statement in propositional logic will correspond to a badly-typed lambda expression. No typed lambdas should be able to witness something false!
+
+What happens if we upgrade and complicate the propositional logic? Consider the predicate logic, which is propositional logic with quantiifers.
+
+Well, since propositional logic is practically 1-to-1 with the simply typed lambda calculus, we will need new constructs to handle the quantifiers. Howard and
+De Bruijn introduced the dependent product and dependent pairs for the universal
+and existential quantiifer, respectively.
+
+```
+∀x:Nat. ∃y:Nat. x < y
+
+-- corresponds to
+
+Π(x: Nat) → Σ(y : Nat) × (x < y)
+```
+
+Here is a crucial question: Logic is more intuitive than the type of some lambda term.
+So are there situations where it would serve us better if we think in terms of type theory rather than logic?
+
+Yes. Type theory is constructive by nature, logic needs not be.
+
+In `Coq`, this means one can extract and compute with `Type` (constructive type theory) but not with `Prop` (logical propositions). 
+For example, given a proof of `A \/ B`, which is defined as an inductive prop, you do not have access to whether an `A` or `B` was constructed to witness `A \/ B`. 
+To obtain the witness, we have to use `orb`, which is the `Type` way of doing things.
+
+As a further example, if you wish to obtain a witness, you must use a dependent pair; if you do not, a regular existential proposition is fine.
+```coq
+Definition foo' (B: Type) P := exists b: B, P b.
+Definition bar' B P (H: foo' B P) : B.
+  unfold fooable in H.
+  destruct H. (* Error here *)
+
+Definition foo'' P := {b: B | P b}.
+Definition bar'' B P (H: foo'' B P) : B.
+  unfold fooable in H.
+  destruct H. (* Just fine *)
+  exact x.
+Qed.
+
+(* Or, we could just stay in prop land, the only diff here is B: Prop)
+Definition foo' (B: Prop) P := exists b: B, P b.
+Definition bar' B P (H: foo' B P) : B.
+  unfold fooable in H.
+  destruct H. (* Error here *)
+```
+
+
+## Resources
+https://en.wikipedia.org/wiki/Dependent_type

src/full_applications/verified_cryptography/cryptol_for_haskell_knowers/front.md

@@ -178,6 +178,16 @@ stream = [0x3F, 0xE2, 0x65, 0xCA] # new
 Soak in the beauty for a bit, then, think carefully about how laziness enables this code. Beware of showing this to your imperative friends.
 > Those who were seen dancing were thought to be insane by those who could not hear the music.
 
+More generally,
+```haskell
+ys = [i] # [ f (x, y) | x <- xs
+                      | y <- ys
+]
+```
+where `xs` is some input sequence, `i` is the result corresponding to the empty sequence, and `f` is a transformer to compute the next element, using the previous result and the next input.
+
+
+
 
 ### Using Type in Variable Context
 

src/glossary_resources.md

@@ -0,0 +1,5 @@
+# Glossary and Resources
+
+## Resources
+[Model Checking](https://mitpress.ublish.com/ebook/model-checking-2e-preview/7092/ix): Temporal Logics, Automata, SAT, \\( \mu \\)-Calculus, concurrency
+