Please enable JavaScript.
Coggle requires JavaScript to display documents.
TOC Week 10, A term with no free variables is closed, PITFALLS: When…
TOC Week 10
-
We can get terms which make no sense but are correct in terms of our untyped lambda calculus. Some terms have a normal form but won't evaluate to it because they evaluate the argument to a function first and get stuck or run forever
We prevent this by restricting the language to well-typed terms - to do this, we need a type system
-
-
TYPE INFERENCE: sometimes we can assume the type of an untyped term using context clues but we also sometimes get contradictions such as applying an integer to something meaning it needs to be of type A-->B but is also an int
-
-
Currying: to express multiary functions in lambda calculus, we make use of currying - representing a function with two arguments as a function that returns a function, and so forth (recursive)
-
Two terms are said to be alpha equivalent if they're the same other than bound variables (which should still be bound to the same place) and binders. We regard them as the same.
-
PITFALLS: When reducing using outermost beta reduction, its important to only replace free occurrences of your variable (sometimes we use a preliminary alpha conversion). We must also be safe in order to not capture free occurrences of our variable
we stop evaluating when there is no more sigma or beta reduction to be done - this is known as beta sigma normal form