Diagrammatic logics were introduced in 2002, with emphasis on the notions of
specifications and models. In this paper we improve the description of the
inference process, which is seen as a Yoneda functor on a bicategory of
fractions. A diagrammatic logic is defined from a morphism of limit sketches
(called a propagator) which gives rise to an adjunction, which in turn
determines a bicategory of fractions. The propagator, the adjunction and the
bicategory provide respectively the syntax, the models and the inference
process for the logic.
We tackle the problem of graph transformation with a particular focus on node
cloning. We propose a graph rewriting framework where nodes can be cloned zero,
one or more times. A node can be cloned together with all its incident edges,
with only the outgoing edges, with only the incoming edges or without any of
the incident edges. We thus subsume previous works such as the sesqui-pushout,
the heterogeneous pushout and the adaptive star grammars approaches.
This paper is a submission to the contest: How to combine logics? at the
World Congress and School on Universal Logic III, 2010. We claim that combining
"things", whatever these things are, is made easier if these things can be seen
as the objects of a category. We define the category of diagrammatic logics, so
that categorical constructions can be used for combining diagrammatic logics.
As an example, a combination of logics using an opfibration is presented, in
order to study computational side-effects due to the evolution of the state
during the execution of an imperative program.
The parameterization process used in the symbolic computation systems Kenzo
and EAT is studied here as a general construction in a categorical framework.
This parameterization process starts from a given specification and builds a
parameterized specification by adding a parameter as a new variable to some
operations. Given a model of the parameterized specification, each
interpretation of the parameter, called an argument, provides a model of the
given specification.
This paper provides an abstract definition of some kinds of logics, called
diagrammatic logics, together with a definition of morphisms and of 2-morphisms
between diagrammatic logics. The definition of the 2-category of diagrammatic
logics rely on category theory, mainly on adjunction, categories of fractions
and limit sketches. This framework is applied to the formalization of a
parameterization process. This process, which consists in adding a formal
parameter to some operations in a given specification, is presented as a
morphism of logics.