Unification of hypergraph λ-terms

Alimujiang Yasen, Kazunori Ueda

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

    Abstract

    We developed a technique for modeling formal systems involving name binding in a modeling language based on hypergraph rewriting. A hypergraph consists of graph nodes, edges with two endpoints and edges with multiple endpoints. The idea is that hypergraphs allow us to represent terms containing bindings and that our notion of a graph type keeps bound variables distinct throughout rewriting steps. We previously encoded the untyped λ-calculus and the evaluation and type checking of System F<:, but the encoding of System F<: type inference requires a unification algorithm. We studied and successfully implemented a unification algorithm modulo α-equivalence for hypergraphs representing untyped λ-terms. The unification algorithm turned out to be similar to nominal unification despite the fact that our approach and nominal approach to name binding are very different. However, some basic properties of our framework are easier to establish compared to the ones in nominal unification. We believe this indicates that hypergraphs provide a nice framework for encoding formal systems involving binders and unification modulo α-equivalence.

    Original languageEnglish
    Title of host publicationTopics in Theoretical Computer Science - 2nd IFIP WG 1.8 International Conference, TTCS 2017, Proceedings
    PublisherSpringer Verlag
    Pages106-124
    Number of pages19
    Volume10608 LNCS
    ISBN (Print)9783319689524
    DOIs
    Publication statusPublished - 2017
    Event2nd IFIP WG 1.8 International Conference on Topics in Theoretical Computer Science, TTCS 2017 - Tehran, Iran, Islamic Republic of
    Duration: 2017 Sep 122017 Sep 14

    Publication series

    NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
    Volume10608 LNCS
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Other

    Other2nd IFIP WG 1.8 International Conference on Topics in Theoretical Computer Science, TTCS 2017
    CountryIran, Islamic Republic of
    CityTehran
    Period17/9/1217/9/14

    Fingerprint

    Unification
    Hypergraph
    Term
    Categorical or nominal
    Rewriting
    Binders
    Modulo
    Encoding
    Equivalence
    Multiple Endpoints
    Type Inference
    Formal Modeling
    Graph in graph theory
    Modeling Language
    Calculus
    Distinct
    Evaluation
    Vertex of a graph

    ASJC Scopus subject areas

    • Theoretical Computer Science
    • Computer Science(all)

    Cite this

    Yasen, A., & Ueda, K. (2017). Unification of hypergraph λ-terms. In Topics in Theoretical Computer Science - 2nd IFIP WG 1.8 International Conference, TTCS 2017, Proceedings (Vol. 10608 LNCS, pp. 106-124). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10608 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-319-68953-1_9

    Unification of hypergraph λ-terms. / Yasen, Alimujiang; Ueda, Kazunori.

    Topics in Theoretical Computer Science - 2nd IFIP WG 1.8 International Conference, TTCS 2017, Proceedings. Vol. 10608 LNCS Springer Verlag, 2017. p. 106-124 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10608 LNCS).

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

    Yasen, A & Ueda, K 2017, Unification of hypergraph λ-terms. in Topics in Theoretical Computer Science - 2nd IFIP WG 1.8 International Conference, TTCS 2017, Proceedings. vol. 10608 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10608 LNCS, Springer Verlag, pp. 106-124, 2nd IFIP WG 1.8 International Conference on Topics in Theoretical Computer Science, TTCS 2017, Tehran, Iran, Islamic Republic of, 17/9/12. https://doi.org/10.1007/978-3-319-68953-1_9
    Yasen A, Ueda K. Unification of hypergraph λ-terms. In Topics in Theoretical Computer Science - 2nd IFIP WG 1.8 International Conference, TTCS 2017, Proceedings. Vol. 10608 LNCS. Springer Verlag. 2017. p. 106-124. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-319-68953-1_9
    Yasen, Alimujiang ; Ueda, Kazunori. / Unification of hypergraph λ-terms. Topics in Theoretical Computer Science - 2nd IFIP WG 1.8 International Conference, TTCS 2017, Proceedings. Vol. 10608 LNCS Springer Verlag, 2017. pp. 106-124 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
    @inproceedings{457bb7bc17ae4d6c8ad8085badf9e81f,
    title = "Unification of hypergraph λ-terms",
    abstract = "We developed a technique for modeling formal systems involving name binding in a modeling language based on hypergraph rewriting. A hypergraph consists of graph nodes, edges with two endpoints and edges with multiple endpoints. The idea is that hypergraphs allow us to represent terms containing bindings and that our notion of a graph type keeps bound variables distinct throughout rewriting steps. We previously encoded the untyped λ-calculus and the evaluation and type checking of System F<:, but the encoding of System F<: type inference requires a unification algorithm. We studied and successfully implemented a unification algorithm modulo α-equivalence for hypergraphs representing untyped λ-terms. The unification algorithm turned out to be similar to nominal unification despite the fact that our approach and nominal approach to name binding are very different. However, some basic properties of our framework are easier to establish compared to the ones in nominal unification. We believe this indicates that hypergraphs provide a nice framework for encoding formal systems involving binders and unification modulo α-equivalence.",
    author = "Alimujiang Yasen and Kazunori Ueda",
    year = "2017",
    doi = "10.1007/978-3-319-68953-1_9",
    language = "English",
    isbn = "9783319689524",
    volume = "10608 LNCS",
    series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
    publisher = "Springer Verlag",
    pages = "106--124",
    booktitle = "Topics in Theoretical Computer Science - 2nd IFIP WG 1.8 International Conference, TTCS 2017, Proceedings",
    address = "Germany",

    }

    TY - GEN

    T1 - Unification of hypergraph λ-terms

    AU - Yasen, Alimujiang

    AU - Ueda, Kazunori

    PY - 2017

    Y1 - 2017

    N2 - We developed a technique for modeling formal systems involving name binding in a modeling language based on hypergraph rewriting. A hypergraph consists of graph nodes, edges with two endpoints and edges with multiple endpoints. The idea is that hypergraphs allow us to represent terms containing bindings and that our notion of a graph type keeps bound variables distinct throughout rewriting steps. We previously encoded the untyped λ-calculus and the evaluation and type checking of System F<:, but the encoding of System F<: type inference requires a unification algorithm. We studied and successfully implemented a unification algorithm modulo α-equivalence for hypergraphs representing untyped λ-terms. The unification algorithm turned out to be similar to nominal unification despite the fact that our approach and nominal approach to name binding are very different. However, some basic properties of our framework are easier to establish compared to the ones in nominal unification. We believe this indicates that hypergraphs provide a nice framework for encoding formal systems involving binders and unification modulo α-equivalence.

    AB - We developed a technique for modeling formal systems involving name binding in a modeling language based on hypergraph rewriting. A hypergraph consists of graph nodes, edges with two endpoints and edges with multiple endpoints. The idea is that hypergraphs allow us to represent terms containing bindings and that our notion of a graph type keeps bound variables distinct throughout rewriting steps. We previously encoded the untyped λ-calculus and the evaluation and type checking of System F<:, but the encoding of System F<: type inference requires a unification algorithm. We studied and successfully implemented a unification algorithm modulo α-equivalence for hypergraphs representing untyped λ-terms. The unification algorithm turned out to be similar to nominal unification despite the fact that our approach and nominal approach to name binding are very different. However, some basic properties of our framework are easier to establish compared to the ones in nominal unification. We believe this indicates that hypergraphs provide a nice framework for encoding formal systems involving binders and unification modulo α-equivalence.

    UR - http://www.scopus.com/inward/record.url?scp=85032483720&partnerID=8YFLogxK

    UR - http://www.scopus.com/inward/citedby.url?scp=85032483720&partnerID=8YFLogxK

    U2 - 10.1007/978-3-319-68953-1_9

    DO - 10.1007/978-3-319-68953-1_9

    M3 - Conference contribution

    SN - 9783319689524

    VL - 10608 LNCS

    T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

    SP - 106

    EP - 124

    BT - Topics in Theoretical Computer Science - 2nd IFIP WG 1.8 International Conference, TTCS 2017, Proceedings

    PB - Springer Verlag

    ER -