Higher order disunification: Some decidable cases
Identifieur interne : 000E76 ( Istex/Curation ); précédent : 000E75; suivant : 000E77Higher order disunification: Some decidable cases
Auteurs : D. Lugiez [France]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: This paper deals with higher-order disunification, i.e solving constraints on simply typed lambda-terms involving the ηβ equality, negation, the logical connectives ∧ and ∨ and universal and existential quantification. Contrary to the first-order case, higher-order disunification is undecidable and even not semi-decidable since it contains higher-order unification and its negation. Therefore we merely give general rules to simplify the basic constraints called equational problems and we use these rules to get decision procedures in some useful cases. First we prove that the second-order top-linear complement problem and other special cases of complement problems are decidable. Then we consider the case when all the terms involved in the constraints are patterns i.e when the arguments of a free variable are distinct bound variables. In this case, we can devise new rules to extend the initial set of rules, and we are able to prove the decidability of the general case of disunification constraints, i.e involving mixed quantification.
Url:
DOI: 10.1007/BFb0016848
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: Pour aller vers cette notice dans l'étape Curation :000E88
Links to Exploration step
ISTEX:3F0A384E8F0F2A82929E19425E3C554546603B85Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Higher order disunification: Some decidable cases</title>
<author><name sortKey="Lugiez, D" sort="Lugiez, D" uniqKey="Lugiez D" first="D." last="Lugiez">D. Lugiez</name>
<affiliation wicri:level="1"><mods:affiliation>CRIN-INRIA, BP239 54506, Vandoeuvres-les-Nancy, France</mods:affiliation>
<country xml:lang="fr">France</country>
<wicri:regionArea>CRIN-INRIA, BP239 54506, Vandoeuvres-les-Nancy</wicri:regionArea>
</affiliation>
<affiliation wicri:level="1"><mods:affiliation>E-mail: lugiez@loria.fr</mods:affiliation>
<country wicri:rule="url">France</country>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">ISTEX</idno>
<idno type="RBID">ISTEX:3F0A384E8F0F2A82929E19425E3C554546603B85</idno>
<date when="1994" year="1994">1994</date>
<idno type="doi">10.1007/BFb0016848</idno>
<idno type="url">https://api.istex.fr/ark:/67375/HCB-V1P3HBVF-3/fulltext.pdf</idno>
<idno type="wicri:Area/Istex/Corpus">000E88</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">000E88</idno>
<idno type="wicri:Area/Istex/Curation">000E76</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Higher order disunification: Some decidable cases</title>
<author><name sortKey="Lugiez, D" sort="Lugiez, D" uniqKey="Lugiez D" first="D." last="Lugiez">D. Lugiez</name>
<affiliation wicri:level="1"><mods:affiliation>CRIN-INRIA, BP239 54506, Vandoeuvres-les-Nancy, France</mods:affiliation>
<country xml:lang="fr">France</country>
<wicri:regionArea>CRIN-INRIA, BP239 54506, Vandoeuvres-les-Nancy</wicri:regionArea>
</affiliation>
<affiliation wicri:level="1"><mods:affiliation>E-mail: lugiez@loria.fr</mods:affiliation>
<country wicri:rule="url">France</country>
</affiliation>
</author>
</analytic>
<monogr></monogr>
<series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title>
<title level="s" type="abbrev">Lect Notes Comput Sci</title>
<idno type="ISSN">0302-9743</idno>
<idno type="eISSN">1611-3349</idno>
<idno type="ISSN">0302-9743</idno>
</series>
</biblStruct>
</sourceDesc>
<seriesStmt><idno type="ISSN">0302-9743</idno>
</seriesStmt>
</fileDesc>
<profileDesc><textClass></textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">Abstract: This paper deals with higher-order disunification, i.e solving constraints on simply typed lambda-terms involving the ηβ equality, negation, the logical connectives ∧ and ∨ and universal and existential quantification. Contrary to the first-order case, higher-order disunification is undecidable and even not semi-decidable since it contains higher-order unification and its negation. Therefore we merely give general rules to simplify the basic constraints called equational problems and we use these rules to get decision procedures in some useful cases. First we prove that the second-order top-linear complement problem and other special cases of complement problems are decidable. Then we consider the case when all the terms involved in the constraints are patterns i.e when the arguments of a free variable are distinct bound variables. In this case, we can devise new rules to extend the initial set of rules, and we are able to prove the decidability of the general case of disunification constraints, i.e involving mixed quantification.</div>
</front>
</TEI>
</record>
Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Istex/Curation
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000E76 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Curation/biblio.hfd -nk 000E76 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien |wiki= Wicri/Lorraine |area= InforLorV4 |flux= Istex |étape= Curation |type= RBID |clé= ISTEX:3F0A384E8F0F2A82929E19425E3C554546603B85 |texte= Higher order disunification: Some decidable cases }}
This area was generated with Dilib version V0.6.33. |