View in EDS

Proving operational termination of membership equational programs.

Saved in:
Bibliographic Details
Title: Proving operational termination of membership equational programs.
Authors: Francisco Durán1, Salvador Lucas2, Claude Marché3, José Meseguer4, Xavier Urbain5
Source: Higher-Order & Symbolic Computation. Jun2008, Vol. 21 Issue 1/2, p59-88. 30p.
Subjects: Theory, Language & languages, Judgment (Logic), Thought & thinking
Abstract: Abstract  Reasoning about the termination of equational programs in sophisticated equational languages such as Elan, Maude, OBJ, CafeOBJ, Haskell, and so on, requires support for advanced features such as evaluation strategies, rewriting modulo, use of extra variables in conditions, partiality, and expressive type systems (possibly including polymorphism and higher-order). However, many of those features are, at best, only partially supported by current term rewriting termination tools (for instance mu-term, C i ME, AProVE, TTT, Termptation, etc.) while they may be essential to ensure termination. We present a sequence of theory transformations that can be used to bridge the gap between expressive membership equational programs and such termination tools, and prove the correctness of such transformations. We also discuss a prototype tool performing the transformations on Maude equational programs and sending the resulting transformed theories to some of the aforementioned standard termination tools. [ABSTRACT FROM AUTHOR]
Copyright of Higher-Order & Symbolic Computation is the property of Springer Nature and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)
Database: Engineering Source
FullText Text:
  Availability: 0
Header DbId: egs
DbLabel: Engineering Source
An: 33049161
AccessLevel: 6
PubType: Academic Journal
PubTypeId: academicJournal
PreciseRelevancyScore: 0
IllustrationInfo
Items – Name: Title
  Label: Title
  Group: Ti
  Data: Proving operational termination of membership equational programs.
– Name: Author
  Label: Authors
  Group: Au
  Data: <searchLink fieldCode="AR" term="%22Francisco+Durán%22">Francisco Durán</searchLink><relatesTo>1</relatesTo><br /><searchLink fieldCode="AR" term="%22Salvador+Lucas%22">Salvador Lucas</searchLink><relatesTo>2</relatesTo><br /><searchLink fieldCode="AR" term="%22Claude+Marché%22">Claude Marché</searchLink><relatesTo>3</relatesTo><br /><searchLink fieldCode="AR" term="%22José+Meseguer%22">José Meseguer</searchLink><relatesTo>4</relatesTo><br /><searchLink fieldCode="AR" term="%22Xavier+Urbain%22">Xavier Urbain</searchLink><relatesTo>5</relatesTo>
– Name: TitleSource
  Label: Source
  Group: Src
  Data: <searchLink fieldCode="JN" term="%22Higher-Order+%26+Symbolic+Computation%22">Higher-Order & Symbolic Computation</searchLink>. Jun2008, Vol. 21 Issue 1/2, p59-88. 30p.
– Name: Subject
  Label: Subjects
  Group: Su
  Data: <searchLink fieldCode="DE" term="%22Theory%22">Theory</searchLink><br /><searchLink fieldCode="DE" term="%22Language+%26+languages%22">Language & languages</searchLink><br /><searchLink fieldCode="DE" term="%22Judgment+%28Logic%29%22">Judgment (Logic)</searchLink><br /><searchLink fieldCode="DE" term="%22Thought+%26+thinking%22">Thought & thinking</searchLink>
– Name: Abstract
  Label: Abstract
  Group: Ab
  Data: Abstract  Reasoning about the termination of equational programs in sophisticated equational languages such as Elan, Maude, OBJ, CafeOBJ, Haskell, and so on, requires support for advanced features such as evaluation strategies, rewriting modulo, use of extra variables in conditions, partiality, and expressive type systems (possibly including polymorphism and higher-order). However, many of those features are, at best, only partially supported by current term rewriting termination tools (for instance mu-term, C i ME, AProVE, TTT, Termptation, etc.) while they may be essential to ensure termination. We present a sequence of theory transformations that can be used to bridge the gap between expressive membership equational programs and such termination tools, and prove the correctness of such transformations. We also discuss a prototype tool performing the transformations on Maude equational programs and sending the resulting transformed theories to some of the aforementioned standard termination tools. [ABSTRACT FROM AUTHOR]
– Name: AbstractSuppliedCopyright
  Label:
  Group: Ab
  Data: <i>Copyright of Higher-Order & Symbolic Computation is the property of Springer Nature and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract.</i> (Copyright applies to all Abstracts.)
PLink https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=33049161
RecordInfo BibRecord:
  BibEntity:
    Languages:
      – Code: eng
        Text: English
    PhysicalDescription:
      Pagination:
        PageCount: 30
        StartPage: 59
    Subjects:
      – SubjectFull: Theory
        Type: general
      – SubjectFull: Language & languages
        Type: general
      – SubjectFull: Judgment (Logic)
        Type: general
      – SubjectFull: Thought & thinking
        Type: general
    Titles:
      – TitleFull: Proving operational termination of membership equational programs.
        Type: main
  BibRelationships:
    HasContributorRelationships:
      – PersonEntity:
          Name:
            NameFull: Francisco Durán
      – PersonEntity:
          Name:
            NameFull: Salvador Lucas
      – PersonEntity:
          Name:
            NameFull: Claude Marché
      – PersonEntity:
          Name:
            NameFull: José Meseguer
      – PersonEntity:
          Name:
            NameFull: Xavier Urbain
    IsPartOfRelationships:
      – BibEntity:
          Dates:
            – D: 29
              M: 06
              Text: Jun2008
              Type: published
              Y: 2008
          Identifiers:
            – Type: issn-print
              Value: 13883690
          Numbering:
            – Type: volume
              Value: 21
            – Type: issue
              Value: 1/2
          Titles:
            – TitleFull: Higher-Order & Symbolic Computation
              Type: main
ResultId 1