InforLorV4, Main, Exploration, bibRecordById, Pascal:10-0210395

Static Dependency Pair Method Based on Strong Computability for Higher-Order Rewrite Systems

Identifieur interne : 003B65 ( Main/Exploration ); précédent : 003B64; suivant : 003B66

Static Dependency Pair Method Based on Strong Computability for Higher-Order Rewrite Systems

Auteurs : Keiichirou Kusakari [Japon] ; Yasuo Isogai [Japon] ; Masahiko Sakai [Japon] ; Frédéric Blanqui [France]

Source :

IEICE transactions on information and systems [ 0916-8532 ] ; 2009.

RBID : Pascal:10-0210395

Descripteurs français

Pascal (Inist)
- Calculabilité, Système réécriture, Traitement donnée.

English descriptors

KwdEn :
- Computability, Data processing, Rewriting systems.

Abstract

Higher-order rewrite systems (HRSs) and simply-typed term rewriting systems (STRSs) are computational models of functional programs. We recently proposed an extremely powerful method, the static dependency pair method, which is based on the notion of strong computability, in order to prove termination in STRSs. In this paper, we extend the method to HRSs. Since HRSs include λ-abstraction but STRSs do not, we restructure the static dependency pair method to allow λ-abstraction, and show that the static dependency pair method also works well on HRSs without new restrictions.

Affiliations:

France, Japon

Links toward previous steps (curation, corpus...)

to stream PascalFrancis, to step Corpus: 000219
to stream PascalFrancis, to step Curation: 000800
to stream PascalFrancis, to step Checkpoint: 000227
to stream Main, to step Merge: 003C61
to stream Main, to step Curation: 003B65

Le document en format XML

<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">Static Dependency Pair Method Based on Strong Computability for Higher-Order Rewrite Systems</title>
<author><name sortKey="Kusakari, Keiichirou" sort="Kusakari, Keiichirou" uniqKey="Kusakari K" first="Keiichirou" last="Kusakari">Keiichirou Kusakari</name>
<affiliation wicri:level="1"><inist:fA14 i1="01"><s1>Graduate School of Information Science, Nagoya Univ.</s1>
<s2>Nagoya-shi, 464-8601</s2>
<s3>JPN</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</inist:fA14>
<country>Japon</country>
<wicri:noRegion>Nagoya-shi, 464-8601</wicri:noRegion>
</affiliation>
</author>
<author><name sortKey="Isogai, Yasuo" sort="Isogai, Yasuo" uniqKey="Isogai Y" first="Yasuo" last="Isogai">Yasuo Isogai</name>
<affiliation wicri:level="1"><inist:fA14 i1="01"><s1>Graduate School of Information Science, Nagoya Univ.</s1>
<s2>Nagoya-shi, 464-8601</s2>
<s3>JPN</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</inist:fA14>
<country>Japon</country>
<wicri:noRegion>Nagoya-shi, 464-8601</wicri:noRegion>
</affiliation>
</author>
<author><name sortKey="Sakai, Masahiko" sort="Sakai, Masahiko" uniqKey="Sakai M" first="Masahiko" last="Sakai">Masahiko Sakai</name>
<affiliation wicri:level="1"><inist:fA14 i1="01"><s1>Graduate School of Information Science, Nagoya Univ.</s1>
<s2>Nagoya-shi, 464-8601</s2>
<s3>JPN</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</inist:fA14>
<country>Japon</country>
<wicri:noRegion>Nagoya-shi, 464-8601</wicri:noRegion>
</affiliation>
</author>
<author><name sortKey="Blanqui, Frederic" sort="Blanqui, Frederic" uniqKey="Blanqui F" first="Frédéric" last="Blanqui">Frédéric Blanqui</name>
<affiliation wicri:level="1"><inist:fA14 i1="02"><s1>INRIA & LORIA</s1>
<s3>FRA</s3>
<sZ>4 aut.</sZ>
</inist:fA14>
<country>France</country>
<wicri:noRegion>INRIA & LORIA</wicri:noRegion>
<wicri:noRegion>INRIA & LORIA</wicri:noRegion>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">INIST</idno>
<idno type="inist">10-0210395</idno>
<date when="2009">2009</date>
<idno type="stanalyst">PASCAL 10-0210395 INIST</idno>
<idno type="RBID">Pascal:10-0210395</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000219</idno>
<idno type="wicri:Area/PascalFrancis/Curation">000800</idno>
<idno type="wicri:Area/PascalFrancis/Checkpoint">000227</idno>
<idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000227</idno>
<idno type="wicri:doubleKey">0916-8532:2009:Kusakari K:static:dependency:pair</idno>
<idno type="wicri:Area/Main/Merge">003C61</idno>
<idno type="wicri:Area/Main/Curation">003B65</idno>
<idno type="wicri:Area/Main/Exploration">003B65</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">Static Dependency Pair Method Based on Strong Computability for Higher-Order Rewrite Systems</title>
<author><name sortKey="Kusakari, Keiichirou" sort="Kusakari, Keiichirou" uniqKey="Kusakari K" first="Keiichirou" last="Kusakari">Keiichirou Kusakari</name>
<affiliation wicri:level="1"><inist:fA14 i1="01"><s1>Graduate School of Information Science, Nagoya Univ.</s1>
<s2>Nagoya-shi, 464-8601</s2>
<s3>JPN</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</inist:fA14>
<country>Japon</country>
<wicri:noRegion>Nagoya-shi, 464-8601</wicri:noRegion>
</affiliation>
</author>
<author><name sortKey="Isogai, Yasuo" sort="Isogai, Yasuo" uniqKey="Isogai Y" first="Yasuo" last="Isogai">Yasuo Isogai</name>
<affiliation wicri:level="1"><inist:fA14 i1="01"><s1>Graduate School of Information Science, Nagoya Univ.</s1>
<s2>Nagoya-shi, 464-8601</s2>
<s3>JPN</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</inist:fA14>
<country>Japon</country>
<wicri:noRegion>Nagoya-shi, 464-8601</wicri:noRegion>
</affiliation>
</author>
<author><name sortKey="Sakai, Masahiko" sort="Sakai, Masahiko" uniqKey="Sakai M" first="Masahiko" last="Sakai">Masahiko Sakai</name>
<affiliation wicri:level="1"><inist:fA14 i1="01"><s1>Graduate School of Information Science, Nagoya Univ.</s1>
<s2>Nagoya-shi, 464-8601</s2>
<s3>JPN</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</inist:fA14>
<country>Japon</country>
<wicri:noRegion>Nagoya-shi, 464-8601</wicri:noRegion>
</affiliation>
</author>
<author><name sortKey="Blanqui, Frederic" sort="Blanqui, Frederic" uniqKey="Blanqui F" first="Frédéric" last="Blanqui">Frédéric Blanqui</name>
<affiliation wicri:level="1"><inist:fA14 i1="02"><s1>INRIA & LORIA</s1>
<s3>FRA</s3>
<sZ>4 aut.</sZ>
</inist:fA14>
<country>France</country>
<wicri:noRegion>INRIA & LORIA</wicri:noRegion>
<wicri:noRegion>INRIA & LORIA</wicri:noRegion>
</affiliation>
</author>
</analytic>
<series><title level="j" type="main">IEICE transactions on information and systems</title>
<title level="j" type="abbreviated">IEICE trans. inf. syst.</title>
<idno type="ISSN">0916-8532</idno>
<imprint><date when="2009">2009</date>
</imprint>
</series>
</biblStruct>
</sourceDesc>
<seriesStmt><title level="j" type="main">IEICE transactions on information and systems</title>
<title level="j" type="abbreviated">IEICE trans. inf. syst.</title>
<idno type="ISSN">0916-8532</idno>
</seriesStmt>
</fileDesc>
<profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Computability</term>
<term>Data processing</term>
<term>Rewriting systems</term>
</keywords>
<keywords scheme="Pascal" xml:lang="fr"><term>Calculabilité</term>
<term>Système réécriture</term>
<term>Traitement donnée</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">Higher-order rewrite systems (HRSs) and simply-typed term rewriting systems (STRSs) are computational models of functional programs. We recently proposed an extremely powerful method, the static dependency pair method, which is based on the notion of strong computability, in order to prove termination in STRSs. In this paper, we extend the method to HRSs. Since HRSs include λ-abstraction but STRSs do not, we restructure the static dependency pair method to allow λ-abstraction, and show that the static dependency pair method also works well on HRSs without new restrictions.</div>
</front>
</TEI>
<affiliations><list><country><li>France</li>
<li>Japon</li>
</country>
</list>
<tree><country name="Japon"><noRegion><name sortKey="Kusakari, Keiichirou" sort="Kusakari, Keiichirou" uniqKey="Kusakari K" first="Keiichirou" last="Kusakari">Keiichirou Kusakari</name>
</noRegion>
<name sortKey="Isogai, Yasuo" sort="Isogai, Yasuo" uniqKey="Isogai Y" first="Yasuo" last="Isogai">Yasuo Isogai</name>
<name sortKey="Sakai, Masahiko" sort="Sakai, Masahiko" uniqKey="Sakai M" first="Masahiko" last="Sakai">Masahiko Sakai</name>
</country>
<country name="France"><noRegion><name sortKey="Blanqui, Frederic" sort="Blanqui, Frederic" uniqKey="Blanqui F" first="Frédéric" last="Blanqui">Frédéric Blanqui</name>
</noRegion>
</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 003B65 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 003B65 | 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é=     Pascal:10-0210395
   |texte=   Static Dependency Pair Method Based on Strong Computability for Higher-Order Rewrite Systems
}}

This area was generated with Dilib version V0.6.33.
Data generation: Mon Jun 10 21:56:28 2019. Site generation: Fri Feb 25 15:29:27 2022

	Serveur d'exploration sur la recherche en informatique en Lorraine
	Attention, ce site est en cours de développement ! Attention, site généré par des moyens informatiques à partir de corpus bruts. Les informations ne sont donc pas validées.

Serveur d'exploration sur la recherche en informatique en Lorraine

Static Dependency Pair Method Based on Strong Computability for Higher-Order Rewrite Systems

Static Dependency Pair Method Based on Strong Computability for Higher-Order Rewrite Systems

Source :

Descripteurs français

English descriptors

Abstract

Links toward previous steps (curation, corpus...)

Le document en format XML

Pour manipuler ce document sous Unix (Dilib)

Pour mettre un lien sur cette page dans le réseau Wicri