Seminar 2013-11-19
My goals:
- form an intuition of opetopic sets
- sketch a calculus of (string) diagrams
- discuss the missing piece of cartesian closure
- potential applications to Ωmega 2.0
Mid-1990'es by Baez and Dolan (metatree, opetope), published as arXiv:q-alg/9702014.
TQFTs arXiv:q-alg/9503002
Various researchers/groups contributed since, and similar concepts go by a multitude of names
- Multitopes – Hermida, Makkai
- Opetopes – Eugenia Cheng (e.g. arXiv:math/0304284)
- "positive-to-one computads" – Marek Zawadowski, arXiv:0708.2658
- Szawiel, Marek Zawadowski arXiv:1011.2374
- Joachim Kock, et al. arXiv:0706.1033
At IAS:
- Krzysztof Kapulkin
- Eric Finster
Polynomial functors and monads (iterated construction)
We define zooms as configurable 'tree transformers'.
Then we compose zooms to compexes, subject to boundary conditions.
Input data: finite rooted (planar) trees (the nth dimension)
Freely decorate with disks, adhering to rules:
- disk must cut branch(es), but nothing else
- every disk must capture a subtree
Translate to tree in the (n+1)th dimension
| Input | Output | |
|---|---|---|
| branch | ⊣ | |
| dot | ⇒ | (unit) branch |
| disk | ⇒ | dot |
A corolla is a special zoom with just one dot in the left tree and no disks.
The output tree is thus a unit branch:
The trees have labelled branches and dots (without repetition)
Zooms can be joined when the trees match, forming a zoom complex.
Note: These complexes form a semicategory, as there are input trees not admitting an identity zoom (e.g. unit tree, most corollas).
A zoom complex with dimensions
| -2 | -1 | … | n+1 |
|---|---|---|---|
| O | (.) | . |
and a corolla appearing in the last dimension is called an opetope.
Opetopes are normally drawn starting with dimension 0.
- a 0-dimensional opetope is (isomorphic to) a natural number
- the zoom in dimension 1 has a planar tree input
You can construct opetopes interactively.
Finster gives data type + typechecker
But intrinsic definition
of Zooms is possible.
Similarly defined as the category of singular complexes ∆
-
Morphisms are face maps (corresponding to each 'round-ish thing')
-
Identity morphism (the top cell)
To mark (e.g.) a dot in a tree we use trees that only have one unit branch
"pointer" tree to mark a unit branch
then graft
Mark an n-ary node (or disk), swap it for an n-ary tree
Analogous to monadic bind.
As pasting diagrams.
As string diagrams (dual to the above).
Automatically "type-checked"
Let's have a formal language whose 'terms' are pasting diagrams.
We (say) start out with a set of basic opetopes (axioms).
What are the deduction rules to create new ones?
N.B.: How deductions (proof trees) map to adjuctions in is nicely described here.
From any opetope one can derive an empty pasting diagram one dimension up.
See the corolla zoom. It only shows the highest-dimensional zoom, but that is ok as nothing below changes.
Given n pasting diagrams and a cell (corolla) with n branches
- such that the target cells of the pasting diagrams match the (input) branches
- then a bigger pasting diagram can be created
See pointer guided composition, which is the atomic operation underlying this rule.
Similar to the J-rule
Tensor product on operads http://arxiv.org/pdf/math/0701293.pdf
Boardman-Vogt tensoring: http://arxiv.org/pdf/1302.3711.pdf
Operator categories: http://arxiv.org/pdf/1302.5756.pdf
Symmetric monoidal closed, yes, but cartesian?
- Gambino and Joyal: http://www1.maths.leeds.ac.uk/~pmtng/Research/Lectures/gambino-bmc.pdf
Several notations, e.g. λ (with μ), item notation (Kamareddine, Nederpelt)
let's come up with another one! (…see also Zena Ariola…)
We start with a lambda term
Respecting scope we build a search tree and retrofit it with references
Kind for shapes
kind Sh = Ap Sh Sh | Lm Sh | Rf Ref
kind Ref = Up Ref | Stop | Left Ref | Right Ref | Down RefKey insight: Trees admit naturals
But we need deBruijn + extra sauce
- gluing an input on a (constructor) application ⟶ pattern matching
- … means: "application dot" here
- gluing inputs vanish from application dot
- n-ary application possible? semantics?
When a selected external branch is saturated by application, it completely dissolves, and the addressed binding station gets glued to the argument.
Depending on the intended reduction strategy the use references may be expanded (unsharing).
(→) is binary type constructor
- profunctor (contra-/covariant)
- Klein bottle (orientation-reversing)
Kind promotion
data {- kind -} Nat = Z | S Nat
data Nat' :: Nat -> * where
Z' :: Nat' Z
S' :: Nat' n -> Nat' (S n)Kind definitions possible (at any level)
kind Nat = Z | S Nat
data Nat' :: Nat ~> * where
Z' :: Nat' Z
S' :: Nat' n -> Nat' (S n)data Nat :: level k . *k where
Z :: Nat
S :: Nat ~> Nat
C-H lost as level-polymorphic type Nat above has no type parameter/index!
Idea: parametrize with the same thing, but from one level up...
Unfortunately this is not working out :-(
I tried:
For a few levels (each differently named) it can be made.
parametrize on the left. Make access to parameter optional.
these all mean the same thing:
S Z :: Nat
S Z :: S Z ° Nat
S Z :: (S Z :: Nat) ° Nat
S Z :: (S Z :: S Z ° Nat) ° NatAd infinitum, coinductively.
Program in the (co)limit. Write a very simple data definition
data Nat = Z | S Nat… but have the refinement structure available when wanting to state type-level propositions.
- Opetopic calculus is rich and very interesting
- It appears to be a solid basis for stratified type systems
- Cartesian closure not completely understood yet
Thanks for your attention!
Btw. I am looking for collaborators
- to make these ideas precise
- kick-start an initial implementation.