Abstract
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.
| Original language | English |
|---|---|
| Title of host publication | Proceedings - 10th International Symposium on Theoretical Aspects of Software Engineering, TASE 2016 |
| Publisher | Institute of Electrical and Electronics Engineers Inc. |
| Pages | 113-116 |
| Number of pages | 4 |
| ISBN (Electronic) | 9781509017638 |
| DOIs | |
| Publication status | Published - 2016 Aug 10 |
| Event | 10th International Symposium on Theoretical Aspects of Software Engineering, TASE 2016 - Shanghai, China Duration: 2016 Jul 17 → 2016 Jul 19 |
Other
| Other | 10th International Symposium on Theoretical Aspects of Software Engineering, TASE 2016 |
|---|---|
| Country | China |
| City | Shanghai |
| Period | 16/7/17 → 16/7/19 |
Fingerprint
Keywords
- Graph types
- Hypergraphs
- Substitution
- Terms
ASJC Scopus subject areas
- Computational Theory and Mathematics
- Software
Cite this
Hypergraph Representation of Lambda-Terms. / Yasen, Alimujiang; Ueda, Kazunori.
Proceedings - 10th International Symposium on Theoretical Aspects of Software Engineering, TASE 2016. Institute of Electrical and Electronics Engineers Inc., 2016. p. 113-116 7541894.Research output: Chapter in Book/Report/Conference proceeding › Conference contribution
}
TY - GEN
T1 - Hypergraph Representation of Lambda-Terms
AU - Yasen, Alimujiang
AU - Ueda, Kazunori
PY - 2016/8/10
Y1 - 2016/8/10
N2 - 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.
AB - 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.
KW - Graph types
KW - Hypergraphs
KW - Substitution
KW - Terms
UR - http://www.scopus.com/inward/record.url?scp=84987958752&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84987958752&partnerID=8YFLogxK
U2 - 10.1109/TASE.2016.25
DO - 10.1109/TASE.2016.25
M3 - Conference contribution
AN - SCOPUS:84987958752
SP - 113
EP - 116
BT - Proceedings - 10th International Symposium on Theoretical Aspects of Software Engineering, TASE 2016
PB - Institute of Electrical and Electronics Engineers Inc.
ER -