Authors
Steven Keuchel
Description
Steven Keuchel Page 1 Variables InBound Steven Keuchel Page 2 Binding Page 3 f(x) = x + 1
10 ∑ Mathematics x + 1 10 ∑ k=1 (k + 1) 2 /(x) = x + 1 /(0) = 0 + 1 /(1) = 1 + 1 /(2) = 2 + 1 ... 10
∑ k=1 (1 + 1) 2 + ... + (10 + 1) 2 ff Variable binding Identifiers that can be substituted (for
values) Page 4 Lambda calculus λf.λg.λx. fx (gx) Name binding Identifiers that refer to entities.
static <T> Set<T> singleton(T o) { ... } Type variables in Java Page 5 Metatheory • Programming
languages • Process calculi Metaprogramming • Compilers • Proof assistants • (E)DSLs Page
6 Lambda calculus Page 7 x ∷= <set of variables> t ∷= x | λx.t | t₁ t₂ s := λf.λg.λx.fx (gx)
Syntax Examples Page 8 Haskell representation data LamF = VarF String | AbsF String LamF
| AppF LamF LamF Example s ∷ LamF s = AbsF “f” . AbsF “g” . AbsF “x” $ AppF (AppF (VarF
“f”) (VarF “x”)) (AppF (VarF ”g”) (VarF “x”)) Page 9 Example s ∷ LamF s = AbsF “f” . AbsF “…
Scholar articles