One or Nothing: Anti-unification over the Simply-Typed Lambda Calculus

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985807%3A_____%2F24%3A00585025" target="_blank" >RIV/67985807:_____/24:00585025 - isvavai.cz</a>

Výsledek na webu

<a href="https://doi.org/10.1145/3654798" target="_blank" >https://doi.org/10.1145/3654798</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1145/3654798" target="_blank" >10.1145/3654798</a>

Jazyk výsledku

angličtina

Název v původním jazyce

One or Nothing: Anti-unification over the Simply-Typed Lambda Calculus

Popis výsledku v původním jazyce

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 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 nullary (using capture-avoiding substitutions), even when the arguments to free variables are severely restricted.

Název v anglickém jazyce

One or Nothing: Anti-unification over the Simply-Typed Lambda Calculus

Popis výsledku anglicky

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 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 nullary (using capture-avoiding substitutions), even when the arguments to free variables are severely restricted.

Druh

J_imp - Článek v periodiku v databázi Web of Science

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

<a href="/cs/project/GF22-06414L" target="_blank" >GF22-06414L: Analýza důkazů a automatická dedukce pro rekurzivní struktury</a><br>

Návaznosti

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2024

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název periodika

ACM Transactions on Computational Logic

ISSN

1529-3785

e-ISSN

1557-945X

Svazek periodika

25

Číslo periodika v rámci svazku

3

Stát vydavatele periodika

US - Spojené státy americké

Počet stran výsledku

12

Strana od-do

16

Kód UT WoS článku

001293621100002

EID výsledku v databázi Scopus

2-s2.0-85200593026