Home | Blog | Wiki | About

Based on vidoes of lectures by Robert Harper at OPLSS-2019.

Mistakes my own.

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:

1. Abstract syntax tree
2. Statics (type system)
3. 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'