Coherence for bicategorical cartesian closed structure

2021 ◽  
pp. 1-28
Author(s):  
Marcelo Fiore ◽  
Philip Saville
Keyword(s):  
Lambda Calculus ◽  
Conference Paper ◽  
Full Development ◽  
Typed Lambda Calculus ◽  
Closed Structure ◽  
Coherence Theorem ◽  
Cartesian Closed ◽  
Mac Lane ◽  
Parallel Pair

Abstract We prove a strictification theorem for cartesian closed bicategories. First, we adapt Power’s proof of coherence for bicategories with finite bilimits to show that every bicategory with bicategorical cartesian closed structure is biequivalent to a 2-category with 2-categorical cartesian closed structure. Then we show how to extend this result to a Mac Lane-style “all pasting diagrams commute” coherence theorem: precisely, we show that in the free cartesian closed bicategory on a graph, there is at most one 2-cell between any parallel pair of 1-cells. The argument we employ is reminiscent of that used by Čubrić, Dybjer, and Scott to show normalisation for the simply-typed lambda calculus (Čubrić et al., 1998). The main results first appeared in a conference paper (Fiore and Saville, 2020) but for reasons of space many details are omitted there; here we provide the full development.

Categorical models for non-extensional λ-calculi and combinatory logic

1992 ◽  
Vol 2 (3) ◽  
pp. 327-357 ◽  
Author(s):  
Simone Martini
Keyword(s):  
Lambda Calculus ◽  
Second Order ◽  
Combinatory Logic ◽  
Cartesian Closed Category ◽  
Closed Category ◽  
Simple Generalization ◽  
Categorical Models ◽  
Closed Structure ◽  
Cartesian Closed

The notions of weak Cartesian closed category and very weak CCC are introduced by dropping the extensionality (and the naturality) requirements in the adjunction defining the closed structure of a CCC. A number of specific examples of these categories are given. The weak notions are shown to be equivalent from both the semantic and syntactic standpoint to the typed non-extensional lambda-calculus and to the typed Combinatory Logic, extended with surjective pairs. Type-free models are characterized as reflexive objects in wCCCs. Finally, categorical models for the second-order non-extensional calculus are defined, by introducing a simple generalization of the notion of PL-category.

Categorical and algebraic aspects of the intuitionistic modal logic IEL― and its predicate extensions

2020 ◽  
Author(s):  
Daniel Rogozin
Keyword(s):  
Modal Logic ◽  
Type Theory ◽  
Lambda Calculus ◽  
Conference Paper ◽  
Logical Foundations ◽  
Intuitionistic Modal Logic ◽  
Monoidal Functor ◽  
Cover Systems ◽  
Cartesian Closed ◽  
Intuitionistic Version

Abstract The system of intuitionistic modal logic $\textbf{IEL}^{-}$ was proposed by S. Artemov and T. Protopopescu as the intuitionistic version of belief logic (S. Artemov and T. Protopopescu. Intuitionistic epistemic logic. The Review of Symbolic Logic, 9, 266–298, 2016). We construct the modal lambda calculus, which is Curry–Howard isomorphic to $\textbf{IEL}^{-}$ as the type-theoretical representation of applicative computation widely known in functional programming.We also provide a categorical interpretation of this modal lambda calculus considering coalgebras associated with a monoidal functor on a Cartesian closed category. Finally, we study Heyting algebras and locales with corresponding operators. Such operators are used in point-free topology as well. We study complete Kripke–Joyal-style semantics for predicate extensions of $\textbf{IEL}^{-}$ and related logics using Dedekind–MacNeille completions and modal cover systems introduced by Goldblatt (R. Goldblatt. Cover semantics for quantified lax logic. Journal of Logic and Computation, 21, 1035–1063, 2011). The paper extends the conference paper published in the LFCS’20 volume (D. Rogozin. Modal type theory based on the intuitionistic modal logic IEL. In International Symposium on Logical Foundations of Computer Science, pp. 236–248. Springer, 2020).

scholarly journals Relative Full Completeness for Bicategorical Cartesian Closed Structure

2020 ◽  
pp. 277-298 ◽  
Author(s):  
Marcelo Fiore ◽  
Philip Saville
Keyword(s):  
Programming Languages ◽  
Lambda Calculus ◽  
Equational Theory ◽  
Higher Order ◽  
Finite Product ◽  
Semantic Framework ◽  
Finite Products ◽  
Closed Structure ◽  
Cartesian Closed ◽  
Comma Category

AbstractThe glueing construction, defined as a certain comma category, is an important tool for reasoning about type theories, logics, and programming languages. Here we extend the construction to accommodate ‘2-dimensional theories’ of types, terms between types, and rewrites between terms. Taking bicategories as the semantic framework for such systems, we define the glueing bicategory and establish a bicategorical version of the well-known construction of cartesian closed structure on a glueing category. As an application, we show that free finite-product bicategories are fully complete relative to free cartesian closed bicategories, thereby establishing that the higher-order equational theory of rewriting in the simply-typed lambda calculus is a conservative extension of the algebraic equational theory of rewriting in the fragment with finite products only.

scholarly journals Backpropagation in the simply typed lambda-calculus with linear negation

2020 ◽  
Vol 4 (POPL) ◽  
pp. 1-27 ◽  
Author(s):  
Aloïs Brunel ◽  
Damiano Mazza ◽  
Michele Pagani
Keyword(s):  
Lambda Calculus ◽  
Typed Lambda Calculus

The Simply Typed Lambda Calculus

2013 ◽  
pp. 5-54
Author(s):  
Henk Barendregt ◽  
Wil Dekkers ◽  
Richard Statman
Keyword(s):  
Lambda Calculus ◽  
Typed Lambda Calculus

scholarly journals Proof of a Conjecture of S. Mac Lane

1996 ◽  
Vol 3 (61) ◽  
Author(s):  
Sergei Soloviev
Keyword(s):  
Linear Logic ◽  
Sufficient Conditions ◽  
Vector Spaces ◽  
Categorical Equivalence ◽  
Closed Category ◽  
Symmetric Monoidal Closed Category ◽  
Monoidal Closed Category ◽  
Coherence Theorem ◽  
Mac Lane

Some sufficient conditions on a Symmetric Monoidal Closed category K are obtained such that a diagram in a free SMC category generated by the set A of atoms commutes if and only if all its interpretations in K are commutative. In particular, the category of vector spaces on any field satisfies these conditions (only this case was considered in the original Mac Lane conjecture). Instead of diagrams, pairs of derivations in Intuitionistic Multiplicative Linear logic can be considered (together with categorical equivalence). Two derivations of the same sequent are equivalent if and only if all their interpretations in K are equal. In fact, the assignment of values (objects of K) to atoms is defined constructively for each pair of derivations. Taking into account a mistake in R. Voreadou's proof of the "abstract coherence theorem" found by the author, it was necessary to modify her description of the class of non-commutative diagrams in SMC categories; our proof of S. Mac Lane conjecture proves also the correctness of the modified description.

Sign in / Sign up

Export Citation Format

Share Document