L1

Variable in PL:

Just a placeholder.
'Not a thing (yet)'.
Something which is yet to be determined.
Will be filled in later.

Fun fact: Apparently this concept of variables can be traced back to the works of Brahmagupta and Kwarazmi

Though computer programming in general was heavily influenced by mathematics (logic?), general programming ≠ mathematics.

A programming language:

Abstract syntax tree
Statics (type system)
Dynamics (execution)
- How to evaluate terms
- e ⇓ v

Closed terms:

No free variables.
We know everything that is to know if are to evaluate the term.

An example weaking rule:

Any univariant polynomial is also a multivariant polynomial
Any square is also a rectangle

We make the constraint/type less strict. Hence the name 'weakening'.

The expressive power of a programming language arises from its strictures and not from its affordances. Memorize that statement. - Robert Harper

Can't compare variables ∵ it's not stable under substitution. Contraction rule ??

Collatz conjecture: No one knows the termination criterion yet.

Circuit language

Syntax:

e := tt
   | ff
   | e1 ̅∨₁ e2
   | e1 ̅∨₂ e2

̅∨₁ is NOR.

a ̅∨ b = (a ∨ b)'

We need both ̅∨₁ and ̅∨₂. The distinction is important:

̅∨₁: Left operand evaluated first
̅∨₂: Right operand evaluated first

Typing rules (statics):

─────────     ─────────            
 tt: ckt       ff: ckt            



   e1 e2: ckt          e1 e2: ckt
────────────────    ──────────────── 
 e1 ̅∨₁ e2 : ckt      e1 ̅∨₂ e2 : ckt

Semantics (dynamics):

How to evaluate terms.

e ⇓ v where there are no free variables (ie, closed terms).

─────────     ─────────            
 tt ⇓ tt       ff ⇓ ff            



    e1 ⇓ tt           e2 ⇓ tt
───────────────   ───────────────
 e1 ̅∨₁ e2 ⇓ ff     e1 ̅∨₂ e2 ⇓ ff



  e1 ⇓ ff    e2 ⇓ tt       e1 ⇓ ff    e2 ⇓ ff
─────────────────────    ─────────────────────  
    e1 ̅∨₁ e2 ⇓ ff             e1 ̅∨₁ e2 ⇓ tt      



  e2 ⇓ ff    e1 ⇓ tt       e2 ⇓ ff    e1 ⇓ ff
─────────────────────    ─────────────────────  
    e1 ̅∨₂ e2 ⇓ ff             e1 ̅∨₂ e2 ⇓ tt

⊢ e: ckt

then 

∃v ∈ {ff,tt} such that e⇓v

Implementing an SR-latch

SR-Latch

S	R	Output
0	0	Undefined
0	1	0
1	0	1
1	1	Undefined

How to have the feedback?

R ---------|\
           | o------+------ Y
      +----|/       .                   
      |             .                  
      | .............                  
      | .                              
      +-------------+                  
        .           |                  
        .           |                  
        +--|\       |     
           | o------+------ X
S ---------|/

Y = R NOR X
X = S NOR Y

ie,

Y = R NOR (S NOR Y)

A recursive definition.

We need fixpoint. Y-combinator.

Structural rules

Swap:

  x y:ckt ⊢ e:ckt
─────────────────── 
  y x:ckt ⊢ e:ckt

Reflexivity:

─────────────────── 
  e:ckt ⊢ e:ckt

Misc

Inductive definition:
- Least relation that is closed under a set of rules.

Dbt

Fibrate method? (20:25 lec1)
Plotkin's PCF
- https://en.wikipedia.org/wiki/Programming_Computable_Functions

L2

by-name evaluation
- aka lazy evaluation
- Works well for 'negative types' (like function, product) ??
- Arguments not evaluated
  - Because open terms are not evaluated ??
- Self-recursion (as in 'short circuiting' in the case of circuits) possible

λx1:ℕ. λx2:ℕ. if x1 then true else (iszero x2)

by-value evaluation
- Works well for 'positive types'