Hypergraph Representation of Lambda-Terms

Alimujiang Yasen; Kazunori Ueda

doi:10.1109/TASE.2016.25

Hypergraph Representation of Lambda-Terms

Alimujiang Yasen, Kazunori Ueda

School of Fundamental Science and Engineering

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

4 Citations (Scopus)

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	https://doi.org/10.1109/TASE.2016.25
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

Publication series

Name	Proceedings - 10th International Symposium on Theoretical Aspects of Software Engineering, TASE 2016

Other

Other	10th International Symposium on Theoretical Aspects of Software Engineering, TASE 2016
Country/Territory	China
City	Shanghai
Period	16/7/17 → 16/7/19

Keywords

Graph types
Hypergraphs
Substitution
Terms

ASJC Scopus subject areas

Computational Theory and Mathematics
Software

Access to Document

10.1109/TASE.2016.25

Cite this

Yasen, A., & Ueda, K. (2016). Hypergraph Representation of Lambda-Terms. In Proceedings - 10th International Symposium on Theoretical Aspects of Software Engineering, TASE 2016 (pp. 113-116). Article 7541894 (Proceedings - 10th International Symposium on Theoretical Aspects of Software Engineering, TASE 2016). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/TASE.2016.25

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 (Proceedings - 10th International Symposium on Theoretical Aspects of Software Engineering, TASE 2016).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Yasen, A & Ueda, K 2016, Hypergraph Representation of Lambda-Terms. in Proceedings - 10th International Symposium on Theoretical Aspects of Software Engineering, TASE 2016., 7541894, Proceedings - 10th International Symposium on Theoretical Aspects of Software Engineering, TASE 2016, Institute of Electrical and Electronics Engineers Inc., pp. 113-116, 10th International Symposium on Theoretical Aspects of Software Engineering, TASE 2016, Shanghai, China, 16/7/17. https://doi.org/10.1109/TASE.2016.25

Yasen A, Ueda K. Hypergraph Representation of Lambda-Terms. In Proceedings - 10th International Symposium on Theoretical Aspects of Software Engineering, TASE 2016. Institute of Electrical and Electronics Engineers Inc. 2016. p. 113-116. 7541894. (Proceedings - 10th International Symposium on Theoretical Aspects of Software Engineering, TASE 2016). doi: 10.1109/TASE.2016.25

@inproceedings{d6080edaf92244ae9a9aaa9e388e99aa,

title = "Hypergraph Representation of Lambda-Terms",

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.",

keywords = "Graph types, Hypergraphs, Substitution, Terms",

author = "Alimujiang Yasen and Kazunori Ueda",

note = "Publisher Copyright: {\textcopyright} 2016 IEEE.; 10th International Symposium on Theoretical Aspects of Software Engineering, TASE 2016 ; Conference date: 17-07-2016 Through 19-07-2016",

year = "2016",

month = aug,

day = "10",

doi = "10.1109/TASE.2016.25",

language = "English",

series = "Proceedings - 10th International Symposium on Theoretical Aspects of Software Engineering, TASE 2016",

publisher = "Institute of Electrical and Electronics Engineers Inc.",

pages = "113--116",

booktitle = "Proceedings - 10th International Symposium on Theoretical Aspects of Software Engineering, TASE 2016",

}

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

T3 - Proceedings - 10th International Symposium on Theoretical Aspects of Software Engineering, TASE 2016

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.

T2 - 10th International Symposium on Theoretical Aspects of Software Engineering, TASE 2016

Y2 - 17 July 2016 through 19 July 2016

ER -

Hypergraph Representation of Lambda-Terms

Abstract

Publication series

Other

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this