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
EditorsMohammad Reza Mousavi, Jirí Sgall
PublisherSpringer Verlag
Pages106-124
Number of pages19
ISBN (Print)9783319689524
DOIs
Publication statusPublished - 2017 Jan 1
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

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Unification of hypergraph λ-terms'. Together they form a unique fingerprint.

  • Cite this

    Yasen, A., & Ueda, K. (2017). Unification of hypergraph λ-terms. In M. R. Mousavi, & J. Sgall (Eds.), Topics in Theoretical Computer Science - 2nd IFIP WG 1.8 International Conference, TTCS 2017, Proceedings (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