Hypergraph Representation of Lambda-Terms

Alimujiang Yasen, Kazunori Ueda

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    2 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 languageEnglish
    Title of host publicationProceedings - 10th International Symposium on Theoretical Aspects of Software Engineering, TASE 2016
    PublisherInstitute of Electrical and Electronics Engineers Inc.
    Pages113-116
    Number of pages4
    ISBN (Electronic)9781509017638
    DOIs
    Publication statusPublished - 2016 Aug 10
    Event10th International Symposium on Theoretical Aspects of Software Engineering, TASE 2016 - Shanghai, China
    Duration: 2016 Jul 172016 Jul 19

    Other

    Other10th International Symposium on Theoretical Aspects of Software Engineering, TASE 2016
    CountryChina
    CityShanghai
    Period16/7/1716/7/19

    Fingerprint

    Substitution reactions

    Keywords

    • Graph types
    • Hypergraphs
    • Substitution
    • Terms

    ASJC Scopus subject areas

    • Computational Theory and Mathematics
    • Software

    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). [7541894] 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.

    Research output: Chapter in Book/Report/Conference proceedingConference 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, 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 https://doi.org/10.1109/TASE.2016.25
    Yasen, Alimujiang ; Ueda, Kazunori. / Hypergraph Representation of Lambda-Terms. Proceedings - 10th International Symposium on Theoretical Aspects of Software Engineering, TASE 2016. Institute of Electrical and Electronics Engineers Inc., 2016. pp. 113-116
    @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",
    year = "2016",
    month = "8",
    day = "10",
    doi = "10.1109/TASE.2016.25",
    language = "English",
    pages = "113--116",
    booktitle = "Proceedings - 10th International Symposium on Theoretical Aspects of Software Engineering, TASE 2016",
    publisher = "Institute of Electrical and Electronics Engineers Inc.",
    address = "United States",

    }

    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

    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 -