Hypergraph Representation of Lambda-Terms
Alimujiang Yasen, Kazunori Ueda · 2016
Substitution in the λ-calculus is a subtle operation. In a formal description, Barendregt's variable convention isassumed to avoid variable capture, but such an assumption is notwell suited for implementation on computers. We introduce graphrepresentation and manipulation of λ-terms, in which bound andfree variables are encoded by using hyperlinks with differentattributes. A graph type called hlground is generalized to identifythe scope of a term n in substitution m[x:= n], which enablesbound variables and free variables to have suitable behaviorduring the substitution. Our representation of the λ-terms arereadable and the definition of substitution in this technique isfree from any side conditions on the freeness and freshness of variables.