Free Monads, Intrinsic Scoping, and Higher-Order Preunification
Fuente:
arXiv
Enregistré dans:
| Auteur principal: | |
|---|---|
| Format: | Preprint |
| Publié: |
2022
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866910342198591488 |
|---|---|
| author | Kudasov, Nikolai |
| author_facet | Kudasov, Nikolai |
| contents | Type checking algorithms and theorem provers rely on unification algorithms. In presence of type families or higher-order logic, higher-order (pre)unification (HOU) is required. Many HOU algorithms are expressed in terms of $λ$-calculus and require encodings, such as higher-order abstract syntax, which are sometimes not comfortable to work with for language implementors. To facilitate implementations of languages, proof assistants, and theorem provers, we propose a novel approach based on the second-order abstract syntax of Fiore, data types à la carte of Swierstra, and intrinsic scoping of Bird and Patterson. With our approach, an object language is generated freely from a given bifunctor. Then, given an evaluation function and making a few reasonable assumptions on it, we derive a higher-order preunification procedure on terms in the object language. More precisely, we apply a variant of $E$-unification for second-order syntax. Finally, we briefly demonstrate an application of this technique to implement type checking (with type inference) for Martin-Löf Type Theory, a dependent type theory. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2204_05653 |
| institution | arXiv |
| publishDate | 2022 |
| record_format | arxiv |
| spellingShingle | Free Monads, Intrinsic Scoping, and Higher-Order Preunification Kudasov, Nikolai Logic in Computer Science Type checking algorithms and theorem provers rely on unification algorithms. In presence of type families or higher-order logic, higher-order (pre)unification (HOU) is required. Many HOU algorithms are expressed in terms of $λ$-calculus and require encodings, such as higher-order abstract syntax, which are sometimes not comfortable to work with for language implementors. To facilitate implementations of languages, proof assistants, and theorem provers, we propose a novel approach based on the second-order abstract syntax of Fiore, data types à la carte of Swierstra, and intrinsic scoping of Bird and Patterson. With our approach, an object language is generated freely from a given bifunctor. Then, given an evaluation function and making a few reasonable assumptions on it, we derive a higher-order preunification procedure on terms in the object language. More precisely, we apply a variant of $E$-unification for second-order syntax. Finally, we briefly demonstrate an application of this technique to implement type checking (with type inference) for Martin-Löf Type Theory, a dependent type theory. |
| title | Free Monads, Intrinsic Scoping, and Higher-Order Preunification |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2204.05653 |