Matching with Free Function Symbols — A Simple Extension of Matching?
Identifieur interne : 009852 ( Main/Merge ); précédent : 009851; suivant : 009853Matching with Free Function Symbols — A Simple Extension of Matching?
Auteurs : Christophe Ringeissen [France]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: Matching is a solving process which is crucial in declarative (rule-based) programming languages. In order to apply rules, one has to match the left-hand side of a rule with the term to be rewritten. In several declarative programming languages, programs involve operators that may also satisfy some structural axioms. Therefore, their evaluation mechanism must implement powerful matching algorithms working modulo equational theories. In this paper, we show the existence of an equational theory where matching is decidable (resp. finitary) but matching in presence of additional (free) operators is undecidable (resp. infinitary). The interest of this result is to easily prove the existence of a frontier between matching and matching with free operators.
Url:
DOI: 10.1007/3-540-45127-7_21
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 003031
- to stream Istex, to step Curation: 002F92
- to stream Istex, to step Checkpoint: 001E72
Links to Exploration step
ISTEX:CB6E70BD07E59B2FAB3B339D55C5B37B183A637FLe document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Matching with Free Function Symbols — A Simple Extension of Matching?</title>
<author><name sortKey="Ringeissen, Christophe" sort="Ringeissen, Christophe" uniqKey="Ringeissen C" first="Christophe" last="Ringeissen">Christophe Ringeissen</name>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">ISTEX</idno>
<idno type="RBID">ISTEX:CB6E70BD07E59B2FAB3B339D55C5B37B183A637F</idno>
<date when="2001" year="2001">2001</date>
<idno type="doi">10.1007/3-540-45127-7_21</idno>
<idno type="url">https://api.istex.fr/ark:/67375/HCB-57JS9RH6-L/fulltext.pdf</idno>
<idno type="wicri:Area/Istex/Corpus">003031</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">003031</idno>
<idno type="wicri:Area/Istex/Curation">002F92</idno>
<idno type="wicri:Area/Istex/Checkpoint">001E72</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">001E72</idno>
<idno type="wicri:doubleKey">0302-9743:2001:Ringeissen C:matching:with:free</idno>
<idno type="wicri:Area/Main/Merge">009852</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Matching with Free Function Symbols — A Simple Extension of Matching?</title>
<author><name sortKey="Ringeissen, Christophe" sort="Ringeissen, Christophe" uniqKey="Ringeissen C" first="Christophe" last="Ringeissen">Christophe Ringeissen</name>
<affiliation wicri:level="3"><country xml:lang="fr">France</country>
<wicri:regionArea>LORIA — INRIA, 615, rue du Jardin Botanique, BP 101, 54602, Villers-lés-Nancy Cedex</wicri:regionArea>
<placeName><region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
<settlement type="city">Villers-lés-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>
<idno type="ISSN">0302-9743</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: Matching is a solving process which is crucial in declarative (rule-based) programming languages. In order to apply rules, one has to match the left-hand side of a rule with the term to be rewritten. In several declarative programming languages, programs involve operators that may also satisfy some structural axioms. Therefore, their evaluation mechanism must implement powerful matching algorithms working modulo equational theories. In this paper, we show the existence of an equational theory where matching is decidable (resp. finitary) but matching in presence of additional (free) operators is undecidable (resp. infinitary). The interest of this result is to easily prove the existence of a frontier between matching and matching with free operators.</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 009852 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Merge/biblio.hfd -nk 009852 | 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é= ISTEX:CB6E70BD07E59B2FAB3B339D55C5B37B183A637F |texte= Matching with Free Function Symbols — A Simple Extension of Matching? }}
This area was generated with Dilib version V0.6.33. |