Category-based modularisation for equational logic programming

DOI10.1007/S002360050054MaRDI QIDQ1901708zbMATH OpenOpenAlexFDO

Authors Răzvan Diaconescu

Publication date 19 November 1995

Published in Acta Informatica (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s002360050054

zbMATH Keywords

category-based equational logiccategory-based semanticscompiler correctnesscompletenesslogic-based programmingmodularisationsoundness

Mathematics Subject Classification ID

Logic in computer science (03B70) Theories (e.g., algebraic theories), structure, and semantics (18C10) Logic programming (68N17) Theory of compilers and interpreters (68N20) Semantics in the theory of computing (68Q55)

Review text

Although modularisation is basic to modern computing, it has been little studied for logic-based programming. We treat modularisation for equational logic programming using the institution of category-based equational logic in three different ways: (1) to provide a generic satisfaction condition for equational logics; (2) to give a category-based semantics for queries and their solutions; and (3) as an abstract definition of compilation from one (equational) logic programming language to another. Regarding (2), we study soundness and completeness for equational logic programming queries and their solutions. This can be understood as ordinary soundness and completeness in a suitable ``non-logical institution. Soundness holds for all module imports, but completeness only holds for conservative module imports. Category-based equational signatures are seen as modules, and morphisms of such signatures as module imports. Regarding (3), completeness corresponds to compiler correctness. The results of this research applies to languages based on wide class of equational logic systems, including Horn clause logic, with or without equality; all variant of order and many sorted equational logic, including working modulo a set of axioms; constraint logic programming over arbitrary user-defined data types; and any combination of the above. Most importantly, due to the abstraction level, this research gives the possibility to have semantics and to study modularisation for equational logic programming developed over non-conventional structures.

Recommendations

• An introduction to category-based equational logic
• Category-based constraint logic
• Comments on “logic programming with equations”
• scientific article; zbMATH DE number 408807
• Equality, types, modules, and (why not?) generics for logic programming

Cites work

• A simple algebraic proof of the equational interpolation theorem
• An Oxford survey of order sorted algebra
• Axioms for abstract model theory
• Completeness of category-based equational deduction
• Computing with rewrite systems
• scientific article; zbMATH DE number 4018380 (Why is no real title available?)
• scientific article; zbMATH DE number 4130339 (Why is no real title available?)
• scientific article; zbMATH DE number 4180819 (Why is no real title available?)
• scientific article; zbMATH DE number 3941493 (Why is no real title available?)
• scientific article; zbMATH DE number 3945331 (Why is no real title available?)
• scientific article; zbMATH DE number 3970817 (Why is no real title available?)
• scientific article; zbMATH DE number 4037182 (Why is no real title available?)
• scientific article; zbMATH DE number 4053011 (Why is no real title available?)
• scientific article; zbMATH DE number 3714904 (Why is no real title available?)
• scientific article; zbMATH DE number 3769603 (Why is no real title available?)
• scientific article; zbMATH DE number 44213 (Why is no real title available?)
• scientific article; zbMATH DE number 177826 (Why is no real title available?)
• scientific article; zbMATH DE number 522843 (Why is no real title available?)
• scientific article; zbMATH DE number 1142316 (Why is no real title available?)
• scientific article; zbMATH DE number 195102 (Why is no real title available?)
• scientific article; zbMATH DE number 3997131 (Why is no real title available?)
• scientific article; zbMATH DE number 3999262 (Why is no real title available?)
• scientific article; zbMATH DE number 3367095 (Why is no real title available?)
• Institutions: abstract model theory for specification and programming
• On observational equivalence and algebraic specification
• On the existence of free models in abstract algebraic institutions
• Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
• Proving and rewriting
• Quasi-varieties in abstract algebraic institutions
• Specifications in an arbitrary institution
• The formal theory of monads

Cited in

(5)

• Modular design of domain-specific languages using splittings of catamorphisms
• scientific article; zbMATH DE number 408807 (Why is no real title available?)
• Category-based constraint logic
• An introduction to category-based equational logic
• Living without Beth and Craig: Definitions and Interpolants in Description and Modal Logics with Nominals and Role Inclusions

Describes a project that uses

Uses Software

• OBJ3

This page was built for publication: Category-based modularisation for equational logic programming

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1901708)