Skip to content

ggreif/seminar-opetope

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Short Intro to Opetopes

Seminar 2013-11-19

My goals:

  1. form an intuition of opetopic sets
  2. sketch a calculus of (string) diagrams
  3. discuss the missing piece of cartesian closure
  4. potential applications to Ωmega 2.0

Origin

Mid-1990'es by Baez and Dolan (metatree, opetope), published as arXiv:q-alg/9702014.

TQFTs arXiv:q-alg/9503002

Many People

Various researchers/groups contributed since, and similar concepts go by a multitude of names

At IAS:

  • Krzysztof Kapulkin
  • Eric Finster

Higher-dimensional Trees

Polynomial functors and monads (iterated construction)

Zooms and Complexes

We define zooms as configurable 'tree transformers'.

Then we compose zooms to compexes, subject to boundary conditions.

Zoom definition

A typical zoom

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

Input-to-output translation

Just change the perspective!

Translate to tree in the (n+1)th dimension

Input Output
branch
dot (unit) branch
disk dot

Special case: corolla

A corolla is a special zoom with just one dot in the left tree and no disks.

A corolla

The output tree is thus a unit branch:

Corolla in zoom view

Assembling the complex

The trees have labelled branches and dots (without repetition)

Labelled zoom

Zooms can be joined when the trees match, forming a zoom complex.

Formed complex

Note: These complexes form a semicategory, as there are input trees not admitting an identity zoom (e.g. unit tree, most corollas).

Opetope

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.

Inductive Datatypes

Finster gives data type + typechecker

But intrinsic definition of Zooms is possible.

Category of Opetopes

Similarly defined as the category of singular complexes ∆

  • Morphisms are face maps (corresponding to each 'round-ish thing')

  • Identity morphism (the top cell)

Pointers

To mark (e.g.) a dot in a tree we use trees that only have one unit branch

A pointer

Composition

"pointer" tree to mark a unit branch

then graft

Substitution

Mark an n-ary node (or disk), swap it for an n-ary tree

Substitute

Analogous to monadic bind.

Geometric Realization

As pasting diagrams.

Pasting diagram

As string diagrams (dual to the above).

Coherence conditions

Automatically "type-checked"

Deductions (following Finster)

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.

Empty rule

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.

Paste rule

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.

Composite rule

Universal cell introduction

Universal cell elimination

Similar to the J-rule

The power of the universal cell

Can we Obtain Cartesian Closure?

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?

Excursion: Lambda Calculus

Several notations, e.g. λ (with μ), item notation (Kamareddine, Nederpelt)

let's come up with another one! (…see also Zena Ariola…)

Lambda Graph

(Binary) search tree

We start with a lambda term

Respecting scope we build a search tree and retrofit it with references

Y combinator

Kind for shapes

kind Sh = Ap Sh Sh | Lm Sh | Rf Ref
kind Ref = Up Ref | Stop | Left Ref | Right Ref | Down Ref

Abstraction / Binders

Key insight: Trees admit naturals

Glue input

But we need deBruijn + extra sauce

Docking stations

References: Identification, gluing

References

  • gluing an input on a (constructor) application ⟶ pattern matching
  • … means: "application dot" here
  • gluing inputs vanish from application dot
  • n-ary application possible? semantics?

Beta-reduction

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).

Internal Hom

(→) is binary type constructor

  • profunctor (contra-/covariant)
  • Klein bottle (orientation-reversing)

Strata in Ωmega

Type strata

Singleton Types in Haskell

Kind promotion

Nat'

data {- kind -} Nat = Z | S Nat

data Nat' :: Nat -> * where
  Z' :: Nat' Z
  S' :: Nat' n -> Nat' (S n)

Singleton Types in Ωmega

Kind definitions possible (at any level)

Ωmega's Nat'

kind Nat = Z | S Nat

data Nat' :: Nat ~> * where
  Z' :: Nat' Z
  S' :: Nat' n -> Nat' (S n)

Level Polymorphism

data Nat :: level k . *k where
  Z :: Nat
  S :: Nat ~> Nat

Ωmega's level polymorphism

Can we please have Curry-Howard back?

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:

A failure

For a few levels (each differently named) it can be made.

Next idea

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) ° Nat

Ad infinitum, coinductively.

Programming in the Sky

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.

Conclusion

  1. Opetopic calculus is rich and very interesting
  2. It appears to be a solid basis for stratified type systems
  3. Cartesian closure not completely understood yet

Questions?

Thanks for your attention!

Btw. I am looking for collaborators

  1. to make these ideas precise
  2. kick-start an initial implementation.

About

Short Intro to Opetopes

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages