Higher-Order Equational Unification via Explicit Substitutions
Identifieur interne : 00C124 ( Main/Merge ); précédent : 00C123; suivant : 00C125Higher-Order Equational Unification via Explicit Substitutions
Auteurs : Claude Kirchner ; Christophe RingeissenSource :
English descriptors
Abstract
We show how to reduce the higher-order E-unification problem into a first-order unification problem in a union of two non-disjoint equational theories including E and a calculus of explicit substitutions. A rule-based unification procedure in this combined theory is described and may be viewed as an extension of the one initially designed by G. Dowek, T. Hardin and C. Kirchner for performing unification of simply typed Lambda-terms in a first-order setting via a calculus of explicit substitutions. Additional rules are used to deal with the interaction between E and this first-order calculus.
Links toward previous steps (curation, corpus...)
- to stream Crin, to step Corpus: 001F60
- to stream Crin, to step Curation: 001F60
- to stream Crin, to step Checkpoint: 002670
Links to Exploration step
CRIN:kirchner97aLe document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" wicri:score="400">Higher-Order Equational Unification via Explicit Substitutions</title></titleStmt><publicationStmt><idno type="RBID">CRIN:kirchner97a</idno><date when="1997" year="1997">1997</date><idno type="wicri:Area/Crin/Corpus">001F60</idno><idno type="wicri:Area/Crin/Curation">001F60</idno><idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Curation">001F60</idno><idno type="wicri:Area/Crin/Checkpoint">002670</idno><idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Checkpoint">002670</idno><idno type="wicri:Area/Main/Merge">00C124</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en">Higher-Order Equational Unification via Explicit Substitutions</title><author><name sortKey="Kirchner, Claude" sort="Kirchner, Claude" uniqKey="Kirchner C" first="Claude" last="Kirchner">Claude Kirchner</name></author><author><name sortKey="Ringeissen, Christophe" sort="Ringeissen, Christophe" uniqKey="Ringeissen C" first="Christophe" last="Ringeissen">Christophe Ringeissen</name></author></analytic></biblStruct></sourceDesc></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Explicit Substitutions</term><term>Higher-Order Unification</term><term>Lambda-Calculus</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en" wicri:score="2401">We show how to reduce the higher-order E-unification problem into a first-order unification problem in a union of two non-disjoint equational theories including E and a calculus of explicit substitutions. A rule-based unification procedure in this combined theory is described and may be viewed as an extension of the one initially designed by G. Dowek, T. Hardin and C. Kirchner for performing unification of simply typed Lambda-terms in a first-order setting via a calculus of explicit substitutions. Additional rules are used to deal with the interaction between E and this first-order calculus.</div></front></TEI></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Merge
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 00C124 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Merge/biblio.hfd -nk 00C124 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Merge
|type= RBID
|clé= CRIN:kirchner97a
|texte= Higher-Order Equational Unification via Explicit Substitutions
}}
| This area was generated with Dilib version V0.6.33. |  |