The search session has expired. Please query the service again.
Coalgebras for endofunctors 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. 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...
The question of how to combine monads arises naturally in many areas with much recent interest focusing on the coproduct of two monads. In general, the coproduct of arbitrary monads does not always exist. Although a rather general construction was given by Kelly [Bull. Austral. Math. Soc. 22 (1980) 1–83], its generality is reflected in its complexity which limits the applicability of this construction. Following our own research [C. Lüth and N. Ghani, Lect. Notes Artif. Intell. 2309 (2002) 18–32],...
The question of how to combine monads arises naturally in many areas
with much recent interest focusing on the coproduct of two monads.
In general, the coproduct of arbitrary monads does not always exist.
Although a rather general construction was given by
Kelly [Bull. Austral. Math. Soc.22 (1980) 1–83], its generality is reflected in its
complexity which limits the applicability of this construction.
Following our own research [C. Lüth and N. Ghani,
Lect. Notes Artif. Intell.2309 (2002)...
In this paper we argue that for fuzzy unification we need a procedural and declarative semantics (as opposed to the two valued case, where declarative semantics is hidden in the requirement that unified terms are syntactically – letter by letter – identical). We present an extension of the syntactic model of unification to allow near matches, defined using a similarity relation. We work in Hájek’s fuzzy logic in narrow sense. We base our semantics on a formal model of fuzzy logic programming extended...
This text includes the definition and basic notions of product of posets, chain-complete and flat posets, flattening operation, and the existence theorems of recursive call using the flattening operator. First part of the article, devoted to product and flat posets has a purely mathematical quality. Definition 3 allows to construct a flat poset from arbitrary non-empty set [12] in order to provide formal apparatus which eanbles to work with recursive calls within the Mizar langauge. To achieve this...
We show that the standard normalization-by-evaluation construction for the simply-typed -calculus has a natural counterpart for the untyped -calculus, with the central type-indexed logical relation replaced by a “recursively defined” invariant relation, in the style of Pitts. In fact, the construction can be seen as generalizing a computational-adequacy argument for an untyped, call-by-name language to normalization instead of evaluation.In the untyped setting, not all terms have normal forms,...
We show that the standard normalization-by-evaluation construction for the
simply-typed λβη-calculus
has a natural counterpart for the untyped
λβ-calculus, with the central type-indexed logical relation
replaced by a “recursively defined” invariant relation, in
the style of Pitts. In fact, the construction can be seen as
generalizing a computational-adequacy argument for an untyped,
call-by-name language to normalization instead of evaluation.In the untyped setting, not all terms have normal...
The denotational semantics of a programming language which manages fuzzy data is presented. The introduction of blocks poses problems regarding transmission, both for the degree at which the work is carried out and for triangular operations necessary for the evaluation of the degrees of the fuzzy data. We propose some solutions. The possibility of defining linguistic variables is provided.
The basic framework of domain -calculus was formulated in [39] more than ten years ago. This paper provides an improved formulation of a fragment of the -calculus without function space or powerdomain constructions, and studies some open problems related to this -calculus such as decidability and expressive power. A class of language equations is introduced for encoding -formulas in order to derive results related to decidability and expressive power of non-trivial fragments of the domain -calculus....
The basic framework of domain μ-calculus was
formulated in [39] more than ten years ago.
This paper provides an improved formulation of a fragment of the μ-calculus
without function space or powerdomain constructions,
and studies some open problems
related to this μ-calculus such as
decidability and expressive power.
A class of language equations is introduced
for encoding μ-formulas in order to
derive results related to decidability and expressive power of
non-trivial fragments of the domain...
Mainstream object-oriented
languages often fail to provide complete powerful features
altogether, such as, multiple inheritance, dynamic overloading and
copy semantics of inheritance. In this paper we present a core
object-oriented imperative language that integrates all these
features in a formal framework. We define a static type system and a
translation of the language into the meta-language λ_object,, in order
to account for semantic issues and prove type safety of our
proposal.
We show that the FIX type theory introduced by Crole and Pitts
[3] can be encoded in variants of Abadi and Cardelli's
object calculi. More precisely, we show that the FIX type theory
presented with judgements of both equality and operational reduction
can be translated into object calculi, and the translation proved
sound.
The translations we give can be seen as using object calculi as a
metalanguge within which FIX can be represented; an analogy can be
drawn with Martin Löf's Theory of Arities...
The calculus of looping sequences is a formalism for describing the evolution of biological systems by means of term rewriting rules. In this paper we enrich this calculus with a type discipline which preserves some biological properties depending on the minimum and the maximum number of elements of some type requested by the present elements. The type system enforces these properties and typed reductions guarantee that evolution preserves them. As an example, we model the hemoglobin structure and...
The calculus of looping sequences is a formalism for describing the
evolution of biological systems by means of term rewriting rules. In
this paper we enrich this calculus with a type discipline which
preserves some biological properties depending on the minimum and
the maximum number of elements of some type requested by the present elements. The type
system enforces these properties and typed reductions guarantee that
evolution preserves them. As an example, we model the hemoglobin
structure...
Currently displaying 21 –
40 of
98