One or Nothing: Anti-unification over the Simply-Typed Lambda Calculus
Fuente:
arXiv
Guardado en:
| Autores principales: | , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2022
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866910492487843840 |
|---|---|
| author | Cerna, David M. Buran, Michal |
| author_facet | Cerna, David M. Buran, Michal |
| contents | Generalization techniques have many applications, including template construction, argument generalization, and indexing. Modern interactive provers can exploit advancement in generalization methods over expressive type theories to further develop proof generalization techniques and other transformations. So far, investigations concerned with anti-unification (AU) over $λ$-terms and similar type theories have focused on developing algorithms for well-studied variants. These variants forbid the nesting of generalization variables, restrict the structure of their arguments, and are \textit{unitary}. Extending these methods to more expressive variants is important to applications. We consider the case of nested generalization variables and show that the AU problem is \textit{nullary} (using \textit{capture-avoiding} substitutions), even when the arguments to free variables are severely restricted. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2207_08918 |
| institution | arXiv |
| publishDate | 2022 |
| record_format | arxiv |
| spellingShingle | One or Nothing: Anti-unification over the Simply-Typed Lambda Calculus Cerna, David M. Buran, Michal Logic in Computer Science Generalization techniques have many applications, including template construction, argument generalization, and indexing. Modern interactive provers can exploit advancement in generalization methods over expressive type theories to further develop proof generalization techniques and other transformations. So far, investigations concerned with anti-unification (AU) over $λ$-terms and similar type theories have focused on developing algorithms for well-studied variants. These variants forbid the nesting of generalization variables, restrict the structure of their arguments, and are \textit{unitary}. Extending these methods to more expressive variants is important to applications. We consider the case of nested generalization variables and show that the AU problem is \textit{nullary} (using \textit{capture-avoiding} substitutions), even when the arguments to free variables are severely restricted. |
| title | One or Nothing: Anti-unification over the Simply-Typed Lambda Calculus |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2207.08918 |