done
|
next
Graphical lambda-calculus
a
WimpyPoint
presentation owned by
Johnicholas Hines
The usual definition of lambda-terms
We are mostly interested in closed lambda-terms
Actually, we are mostly interested in equivalence classes
Definition of equivalence classes
A different definition of lambda-terms
Examples of lambda-terms
The usual definition of types
A different definition of types
Examples of types
Change the notation for pictures of types
Redrawing ((B->C)->((A->B)->(A->C))
Redrawing ((A->(B->C))->(B->(A->C)))
A surprising observation
The transformation from BCI-nf to their types
Typing B
Typing C
Data structure for implementation
Pseudo-code for parsing BCI-nf terms
Pseudo-code for printing types
Conclusion
change style