Parametric algebraic specifications with Gentzen formulas – from quasi-freeness to free functor semantics

1995 ◽  
Vol 5 (1) ◽  
pp. 69-111 ◽  
Author(s):  
Michael Löwe ◽  
Uwe Wolter
Keyword(s):  
Function Spaces ◽  
Data Type ◽  
Finite Function ◽  
Practical Applications ◽  
Free Objects ◽  
Algebraic Specifications ◽  
Free Construction ◽  
Horn Formulas ◽  
Type Constructor ◽  
Parametric Case

Inspired by the work of S. Kaplan on positive/negative conditional rewriting, we investigate initial semantics for algebraic specifications with Gentzen formulas. Since the standard initial approach is limited to conditional equations (i.e. positive Horn formulas), the notion of semi-initial and quasi-initial algebras is introduced, and it is shown that all specifications with (positive) Gentzen formulas admit quasi-initial models.The whole approach is generalized to the parametric case where quasi-initiality generalizes to quasi-freeness. Since quasi-free objects need not be isomorphic, the persistency requirement is added to obtain a unique semantics for many interesting practical examples. Unique persistent quasi-free semantics can be described as a free construction if the homomorphisms of the parameter category are suitably restricted. Furthermore, it turns out that unique persistent quasi-free semantics applies especially to specifications where the Gentzen formulas can be interpreted as hierarchical positive/negative conditional equations. The data type constructor of finite function spaces is used as an example that does not admit a correct initial semantics, but does admit a correct unique persistent quasi-initial semantics. The example demonstrates that the concepts introduced in this paper might be of some importance in practical applications.

Redfield's Theorems and Multilinear Algebra

1975 ◽  
Vol 27 (3) ◽  
pp. 704-714 ◽  
Author(s):  
Dennis E. White
Keyword(s):  
Decomposition Theorem ◽  
Function Spaces ◽  
Multilinear Algebra ◽  
Finite Function ◽  
Polya's Theorem ◽  
Pólya’S Theorem ◽  
De Bruijn ◽  
Superposition Theorem

1. Introduction. The remarkable 1927 paper by J. H. Redfield [13] which anticipated many recent combinatorial results in Polya counting theory and, in fact, predated Polya's theorem by ten years has been discussed at length by Harary and Palmer [8], Foulkes [5; 6], Sheehan [15; 16] and Read [12], not to mention de Bruijn [3] and others. We shall, in this paper, demonstrate how multilinear techniques may be used in this context. The Redfield superposition theorem and decomposition theorem turn out to be statements about a group acting on finite function spaces, and may thus be dealt with in multilinear terms. We shall prove Redfield's results and an extension due to Foulkes [5].

scholarly journals Adding Alternative Access Paths to Abstract Data Types

2002 ◽  
pp. 256-267 ◽  
Author(s):  
Xavier Franch ◽  
Jordi Marco
Keyword(s):  
Information Hiding ◽  
Data Type ◽  
Modular Structure ◽  
Abstract Data Type ◽  
Abstract Data Types ◽  
Data Types ◽  
Programming Framework ◽  
Algebraic Specifications ◽  
Abstract Data ◽  
Adequate Representation

We present in this paper a proposal for developing efficient programs in the abstract data type (ADT) programming framework, keeping the modular structure of programs and without violating the information hiding principle. The proposal focuses in the concept of “shortcut” as an efficient way of accessing to data, alternative to the access by means of the primitive operations of the ADT. We develop our approach in a particular ADT, a store of items. We define shortcuts in a formal manner, using algebraic specifications interpreted with initial semantics, and so the result has a well-defined meaning and fits in the ADT framework. Efficiency is assured with an adequate representation of the type, which provides O(1) access to items in the store without penalising the primitive operations of the ADT.

scholarly journals Finite function spaces and measures on hypergraphs

1988 ◽  
Vol 68 (2-3) ◽  
pp. 221-244 ◽  
Author(s):  
S.P. Gudder ◽  
G.T. Rüttimann
Keyword(s):  
Function Spaces ◽  
Finite Function

scholarly journals The Use of Sorts in Algebraic Specifications

1992 ◽  
Vol 21 (416) ◽  
Author(s):  
Peter D. Mosses
Keyword(s):  
Algebraic Specification ◽  
Considerable Influence ◽  
Practical Applications ◽  
Algebraic Specifications

Algebraic specification frameworks exploit a variety of sort disciplines. The treatment of sorts has a considerable influence on the ease with which such features as partiality and polymorphism can be specified. This survey gives an accessible overview of various frameworks, focusing on their sort disciplines and assessing their strengths and weaknesses for practical applications. Familiarity with the basic notions of algebraic specification is assumed.

Sign in / Sign up

Export Citation Format

Share Document