A coherence theorem for canonical morphisms in cartesian closed categories

1982 ◽  
Vol 20 (4) ◽  
pp. 2263-2279 ◽  
Author(s):  
A. A. Babaev ◽  
S. V. Solov'ev
Keyword(s):  
Cartesian Closed Categories ◽  
Coherence Theorem ◽  
Cartesian Closed

scholarly journals The number of proofs for a BCK-formula

1993 ◽  
Vol 58 (2) ◽  
pp. 626-628 ◽  
Author(s):  
Yuichi Komori ◽  
Sachio Hirokawa
Keyword(s):  
Normal Form ◽  
Modus Ponens ◽  
Basic Notion ◽  
Type Assignment ◽  
Natural Deduction System ◽  
Cartesian Closed Categories ◽  
Image Position ◽  
Coherence Theorem ◽  
Cartesian Closed ◽  
Necessary And Sufficient

In this note, we give a necessary and sufficient condition for a BCK-formula to have the unique normal form proof.We call implicational propositional formulas formulas for short. BCK-formulas are the formulas which are derivable from axioms B = (a → b) → (c → a) → c → b, C = (a→b→c)→b→a→c, and K = a→b→a by substitution and modus ponens. It is known that the property of being a BCK-formula is decidable (Jaskowski [11, Theorem 6.5], Ben-Yelles [3, Chapter 3, Theorem 3.22], Komori [12, Corollary 6]). The set of BCK-formulas is identical to the set of provable formulas in the natural deduction system with the following two inference rules.Here γ occurs at most once in (→I). By the formulae-as-types correspondence [10], this set is identical to the set of type-schemes of closed BCK-λ-terms. (See [5].) A BCK-λ-term is a λ-term in which no variable occurs twice. Basic notion concerning the type assignment system can be found [4]. Uniqueness of normal form proofs has been known for balanced formulas. (See [2,14].) It is related to the coherence theorem in cartesian closed categories. A formula is balanced when no variable occurs more than twice in it. It was shown in [8] that the proofs of balanced formulas are BCK-proofs. Relevantly balanced formulas were defined in [9], and it was proved that such formulas have unique normal form proofs. Balanced formulas are included in the set of relevantly balanced formulas.

scholarly journals Dynamic game semantics

2020 ◽  
pp. 1-60
Author(s):  
Norihiro Yamada ◽  
Samson Abramsky
Keyword(s):  
Programming Languages ◽  
Functional Programming ◽  
Operational Semantics ◽  
Dynamic Game ◽  
Standard Interpretation ◽  
Functional Programming Languages ◽  
Game Semantics ◽  
Wide Range ◽  
Cartesian Closed Categories ◽  
Cartesian Closed

Abstract The present work achieves a mathematical, in particular syntax-independent, formulation of dynamics and intensionality of computation in terms of games and strategies. Specifically, we give game semantics of a higher-order programming language that distinguishes programmes with the same value yet different algorithms (or intensionality) and the hiding operation on strategies that precisely corresponds to the (small-step) operational semantics (or dynamics) of the language. Categorically, our games and strategies give rise to a cartesian closed bicategory, and our game semantics forms an instance of a bicategorical generalisation of the standard interpretation of functional programming languages in cartesian closed categories. This work is intended to be a step towards a mathematical foundation of intensional and dynamic aspects of logic and computation; it should be applicable to a wide range of logics and computations.

scholarly journals All cartesian closed categories of quasicontinuous domains consist of domains

2015 ◽  
Vol 594 ◽  
pp. 143-150 ◽  
Author(s):  
Xiaodong Jia ◽  
Achim Jung ◽  
Hui Kou ◽  
Qingguo Li ◽  
Haoran Zhao
Keyword(s):  
Cartesian Closed Categories ◽  
Cartesian Closed

scholarly journals Comparing Cartesian closed categories of (core) compactly generated spaces

2004 ◽  
Vol 143 (1-3) ◽  
pp. 105-145 ◽  
Author(s):  
Martín Escardó ◽  
Jimmie Lawson ◽  
Alex Simpson
Keyword(s):  
Cartesian Closed Categories ◽  
Cartesian Closed ◽  
Compactly Generated

scholarly journals Polynomial functors and polynomial monads

2012 ◽  
Vol 154 (1) ◽  
pp. 153-192 ◽  
Author(s):  
NICOLA GAMBINO ◽  
JOACHIM KOCK
Keyword(s):  
Basic Theory ◽  
Polynomial Functors ◽  
Cartesian Closed Categories ◽  
Cartesian Closed ◽  
The Relationship

AbstractWe study polynomial functors over locally cartesian closed categories. After setting up the basic theory, we show how polynomial functors assemble into a double category, in fact a framed bicategory. We show that the free monad on a polynomial endofunctor is polynomial. The relationship with operads and other related notions is explored.

The sequential topology on is not regular

2009 ◽  
Vol 19 (5) ◽  
pp. 943-957 ◽  
Author(s):  
MATTHIAS SCHRÖDER
Keyword(s):  
Open Subset ◽  
Open Problem ◽  
Polish Space ◽  
Topological Spaces ◽  
Computable Analysis ◽  
Topological Properties ◽  
Compact Open Topology ◽  
Cartesian Closed Categories ◽  
Cartesian Closed ◽  
Continuous Functionals

The compact-open topology on the set of continuous functionals from the Baire space to the natural numbers is well known to be zero-dimensional. We prove that the closely related sequential topology on this set is not even regular. The sequential topology arises naturally as the topology carried by the exponential formed in various cartesian closed categories of topological spaces. Moreover, we give an example of an effectively open subset of that violates regularity. The topological properties of are known to be closely related to an open problem in Computable Analysis. We also show that the sequential topology on the space of continuous real-valued functions on a Polish space need not be regular.

Sign in / Sign up

Export Citation Format

Share Document