Standard model semantics for DSL. A data type specification language (Q799366)

The paper presents a second order type extension of first order logic by introducing metavariables for assertions. Semantics is defined by validity in the usual sense, but treating the metavariables like free variables with valuations being relations. Syntax, called DSL for data type specification language, and semantics, called SMS for standard model semantics, are illustrated in a list of examples including finite sets, natural numbers, bounded counters, well-ordered sets, binary trees and others. Comparison with initial and final semantics of data type specification shows that minimal and final algebras are axiomatizable, while initial algebras still form an open question for being properly axiomatized. Sufficient conditions for axiomatizing computable algebras are given. Finally specification of parameterized data types is discussed and applied in giving the semantics of a simple programming language, called WPL for while-program language. The introduction of the paper is somewhat biased expressing a rather schematic view of data type specification. DSL and SMS, instead, are interesting extensions of first order logic suitable to the specific needs of data type specification.