Matching with Free Function Symbols — A Simple Extension of Matching?
Identifieur interne : 009330 ( Main/Exploration ); précédent : 009329; suivant : 009331Matching with Free Function Symbols — A Simple Extension of Matching?
Auteurs : Christophe Ringeissen [France]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
Descripteurs français
- Pascal (Inist)
- Wicri :
- topic : Langage de programmation.
English descriptors
- KwdEn :
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
Affiliations:
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
- to stream Main, to step Merge: 009852
- to stream PascalFrancis, to step Corpus: 000951
- to stream PascalFrancis, to step Curation: 000125
- to stream PascalFrancis, to step Checkpoint: 000899
- to stream Main, to step Merge: 009982
- to stream Main, to step Curation: 009330
Le 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><idno type="wicri:source">INIST</idno><idno type="RBID">Pascal:01-0325403</idno><idno type="wicri:Area/PascalFrancis/Corpus">000951</idno><idno type="wicri:Area/PascalFrancis/Curation">000125</idno><idno type="wicri:Area/PascalFrancis/Checkpoint">000899</idno><idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000899</idno><idno type="wicri:doubleKey">0302-9743:2001:Ringeissen C:matching:with:free</idno><idno type="wicri:Area/Main/Merge">009982</idno><idno type="wicri:Area/Main/Curation">009330</idno><idno type="wicri:Area/Main/Exploration">009330</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><keywords scheme="KwdEn" xml:lang="en"><term>Decidability</term><term>Declarative language</term><term>Equational theory</term><term>Existence theorem</term><term>Knowledge base</term><term>Pattern matching</term><term>Programming language</term><term>Rewriting systems</term><term>Theorem proving</term></keywords><keywords scheme="Pascal" xml:lang="fr"><term>Base connaissance</term><term>Concordance forme</term><term>Décidabilité</term><term>Démonstration théorème</term><term>Langage déclaratif</term><term>Langage programmation</term><term>Système réécriture</term><term>Théorie équationnelle</term><term>Théorème existence</term></keywords><keywords scheme="Wicri" type="topic" xml:lang="fr"><term>Langage de programmation</term></keywords></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><affiliations><list><country><li>France</li></country><region><li>Grand Est</li><li>Lorraine (région)</li></region><settlement><li>Villers-lés-Nancy</li></settlement></list><tree><country name="France"><region name="Grand Est"><name sortKey="Ringeissen, Christophe" sort="Ringeissen, Christophe" uniqKey="Ringeissen C" first="Christophe" last="Ringeissen">Christophe Ringeissen</name></region><name sortKey="Ringeissen, Christophe" sort="Ringeissen, Christophe" uniqKey="Ringeissen C" first="Christophe" last="Ringeissen">Christophe Ringeissen</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 009330 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 009330 | 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:CB6E70BD07E59B2FAB3B339D55C5B37B183A637F
|texte= Matching with Free Function Symbols — A Simple Extension of Matching?
}}
| This area was generated with Dilib version V0.6.33. |  |