1994, English, Article edition: Dynamically-typed computations for order-sorted equational presentations Hintermeier, Claus; Kirchner, Hélène; Kirchner, Claude

User activity

Share to:
 
Bookmark: http://trove.nla.gov.au/version/204170
Physical Description
  • text
Published
  • HAL - CCSD
  • 1994
Language
  • English

Edition details

Title
  • Dynamically-typed computations for order-sorted equational presentations
Author
  • Hintermeier, Claus
  • Kirchner, Hélène
  • Kirchner, Claude
Published
  • HAL - CCSD
  • 1994
Physical Description
  • text
Subjects
Notes
  • Equational presentations with ordered sorts encompass partially defined functions and subtyping information in an algebraic framework. In this work we address the problem of computing in order-sorted algebras, with very few restrictions on the allowed presentations. We adopt the G-algebra framework, where equational, membership and existence formulas can be expressed, and that provides a complete deduction calculus which incorporates the interaction between all these formulas. To practically deal with this calculus, we introduce an operational semantics for G-algebra using rewrite systems over so-called decorated terms, that have assertions concerning the sort membership of any subterm in its head node. Decorated rewrite rules perform equational replacement, decoration rewrite rules enrich the decorations and record sort information. Therefore we use the semantic sort principle, i.e. equal terms belong to equal sorts, rather than the syntactic sort principle that does not use the equational part of a presentation. In order to have a complete and decidable unification on decorated terms, we restrict to sort inheriting theories. The sort inheritance property is undecidable in general but we provide a test to check it on a given presentation. The test provides information on how to extend the presentation in a model conservative way, in order to obtain sort inheritance. then a completion procedure on decorated terms is designed to compute all interactions between equational and membership formulas. When the completion terminates, the resulting set of rewrite rules provides a way to decide equational theorems of the form (t =​ t') and typing theorems of the form (t : A).
  • HAL:inria-00074463, version 1
  • HAL:http:/​/​hal.inria.fr/​inria-00074463/​en/​
Language
  • English
Contributed by
OAIster

Get this edition

  • Set up My libraries

    How do I set up "My libraries"?

    In order to set up a list of libraries that you have access to, you must first login or sign up. Then set up a personal list of libraries from your profile page by clicking on your user name at the top right of any screen.

  • All (1)
  • Unknown (1)
None of your libraries hold this item.
None of your libraries hold this item.
None of your libraries hold this item.
None of your libraries hold this item.
None of your libraries hold this item.
None of your libraries hold this item.
None of your libraries hold this item.
None of your libraries hold this item.

User activity


e.g. test cricket, Perth (WA), "Parkes, Henry"

Separate different tags with a comma. To include a comma in your tag, surround the tag with double quotes.

Be the first to add a tag for this edition

Be the first to add this to a list

Comments and reviews

What are comments? Add a comment

No user comments or reviews for this version

Add a comment