### $94$-пространства.

Skip to main content (access key 's'),
Skip to navigation (access key 'n'),
Accessibility information (access key '0')

Coalgebras have been proposed as formal basis for the semantics of objects in the sense of object-oriented programming. This paper shows that this semantics provides a smooth interpretation for subtyping, a central notion in object-oriented programming. We show that different characterisations of behavioural subtyping found in the literature can conveniently be expressed in coalgebraic terms. We also investigate the subtle difference between behavioural subtyping and refinement.

We give a complete characterization of the class of functions that are the intensional behaviours of primitive recursive (PR) algorithms. This class is the set of primitive recursive functions that have a null basic case of recursion. This result is obtained using the property of ultimate unarity and a geometrical approach of sequential functions on N the set of positive integers.

An alternative (tree-based) semantics for a class of regular expressions is proposed that assigns a central rôle to the + operator and thus to nondeterminism and nondeterministic choice. For the new semantics a consistent and complete axiomatization is obtained from the original axiomatization of regular expressions by Salomaa and by Kozen by dropping the idempotence law for + and the distribution law of • over +.

We study iteration and recursion operators in the denotational semantics of typed λ-calculi derived from the multiset relational model of linear logic. Although these operators are defined as fixpoints of typed functionals, we prove them finitary in the sense of Ehrhard’s finiteness spaces.

An illustration of coinduction in terms of a notion of weak bisimilarity is presented. First, an operational semantics $\mathcal{O}$ for while programs is defined in terms of a final automaton. It identifies any two programs that are weakly bisimilar, and induces in a canonical manner a compositional model $\mathcal{D}$. Next $\mathcal{O}=\mathcal{D}$ is proved by coinduction.

To binary trees, two-ary integers are what usual integers are to natural numbers, seen as unary trees. We can represent two-ary integers as binary trees too, yet with leaves labelled by binary words and with a structural restriction. In a sense, they are simpler than the binary trees, they relativize. Hence, contrary to the extensions known from Arithmetic and Algebra, this integer extension does not make the starting objects more complex. We use a semantic construction to get this extension. This...

This paper proposes an operational semantics for value recursion in the context of monadic metalanguages. Our technique for combining value recursion with computational effects works uniformly for all monads. The operational nature of our approach is related to the implementation of recursion in Scheme and its monadic version proposed by Friedman and Sabry, but it defines a different semantics and does not rely on assignments. When contrasted to the axiomatic approach proposed by Erkök and Launchbury,...

Coalgebras for endofunctors $\mathcal{C}\to \mathcal{C}$ can be used to model classes of object-oriented languages. However, binary methods do not fit directly into this approach. This paper proposes an extension of the coalgebraic framework, namely the use of extended polynomial functors ${\mathcal{C}}^{op}\times \mathcal{C}\to \mathcal{C}$. This extension allows the incorporation of binary methods into coalgebraic class specifications. The paper also discusses how to define bisimulation and invariants for coalgebras of extended polynomial functors and proves many standard...