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

Result code in 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>

Result on the web

<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>

Result language

angličtina

Original language name

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

Original language description

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.

Czech name

—

Czech description

—

Type

J_imp - Article in a specialist periodical, which is included in the Web of Science database

CEP classification

—

OECD FORD branch

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

Project

<a href="/en/project/GF22-06414L" target="_blank" >GF22-06414L: Proof analysis AND Automated deduction FOr REcursive STructures</a><br>

Continuities

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Publication year

2024

Confidentiality

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

Name of the periodical

ACM Transactions on Computational Logic

ISSN

1529-3785

e-ISSN

1557-945X

Volume of the periodical

25

Issue of the periodical within the volume

3

Country of publishing house

US - UNITED STATES

Number of pages

12

Pages from-to

16

UT code for WoS article

001293621100002

EID of the result in the Scopus database

2-s2.0-85200593026