Diagrammatic Inference

TL;DR

This paper refines the understanding of diagrammatic logics by modeling inference as a Yoneda functor within a bicategory framework, linking syntax, models, and inference in a categorical setting, and applies this to computer language semantics.

Contribution

It introduces a new categorical framework for diagrammatic logics using bicategories and Yoneda functors, enhancing the formal description of inference processes.

Findings

Inference process modeled as Yoneda functor on bicategory of fractions

Diagrammatic logic constructed from propagator morphisms of limit sketches

Application to semantics of side effects in programming languages

Abstract

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. Then diagrammatic logics and their morphisms are applied to the semantics of side effects in computer languages.