Higher order disunification: Some decidable cases
Identifieur interne : 00CD22 ( Main/Exploration ); précédent : 00CD21; suivant : 00CD23Higher 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
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 000E88
- to stream Istex, to step Curation: 000E76
- to stream Istex, to step Checkpoint: 002D11
- to stream Main, to step Merge: 00D590
- to stream Main, to step Curation: 00CD22
Le 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></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><idno type="wicri:Area/Istex/Checkpoint">002D11</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">002D11</idno><idno type="wicri:doubleKey">0302-9743:1994:Lugiez D:higher:order:disunification</idno><idno type="wicri:Area/Main/Merge">00D590</idno><idno type="wicri:Area/Main/Curation">00CD22</idno><idno type="wicri:Area/Main/Exploration">00CD22</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="3"><country xml:lang="fr">France</country><wicri:regionArea>CRIN-INRIA, BP239 54506, Vandoeuvres-les-Nancy</wicri:regionArea><placeName><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region><settlement type="city">Vandoeuvres-les-Nancy</settlement></placeName></affiliation><affiliation wicri:level="1"><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><affiliations><list><country><li>France</li></country><region><li>Grand Est</li><li>Lorraine (région)</li></region><settlement><li>Vandoeuvres-les-Nancy</li></settlement></list><tree><country name="France"><region name="Grand Est"><name sortKey="Lugiez, D" sort="Lugiez, D" uniqKey="Lugiez D" first="D." last="Lugiez">D. Lugiez</name></region><name sortKey="Lugiez, D" sort="Lugiez, D" uniqKey="Lugiez D" first="D." last="Lugiez">D. Lugiez</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 00CD22 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 00CD22 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:3F0A384E8F0F2A82929E19425E3C554546603B85
|texte= Higher order disunification: Some decidable cases
}}
| This area was generated with Dilib version V0.6.33. |  |