Unnamed Opetopes

In addition to the \(\textbf{Opt${}^?$}\) derivation rules and their proof tree node counterparts, the following two functions are present:

• UnnamedOpetope.Arrow(): returns the proof tree of the arrow;
• UnnamedOpetope.OpetopicInteger(): returns the proof tree of an opetopic integer (i.e. \(2\)-opetope).

Examples

The arrow

from opetopy.UnnamedOpetope import Arrow, Point, Shift

ar = Shift(Point())

# Faster way:
# >>> ar = Arrow()

print(ar.eval())
print()
print(ar.toTex())

A classic

from opetopy.UnnamedOpetope import address, Graft, OpetopicInteger, OpetopicTree, Shift

classic = Graft(
    Shift(OpetopicInteger(2)),
    OpetopicInteger(2),
    address([['*']])
)
# Faster way:
# >>> classic = OpetopicTree([None, [None, None]])

print(classic.eval())
print()
print(classic.toTex())

Opetopic integers

Recall that for \(n \in \mathbb{N}\):

• if \(n = 0\), then \(\mathbf{n} = \{ \{ \blacklozenge\);
• if \(n = 1\), then \(\mathbf{n} = \{ [] \leftarrow \blacksquare\);
• otherwise, \(\mathbf{n} = \mathbf{(n-1)} \circ_{[* \cdots *]} \blacksquare\), where there is \((n-1)\) instances of \(*\) in the grafting address.

This is exactly the implementation of UnnamedOpetope.OpetopicInteger().

import sys
sys.path.insert(0, "../")

from opetopy.UnnamedOpetope import OpetopicInteger

oi5 = OpetopicInteger(5)

print(oi5.eval())
print()
print(oi5.toTex())

Deciding opetopes

The UnnamedOpetope.ProofTree() effectively decides opetopes among preopetopes. It takes as argument a preopetopes in “convenient form” (see examples), and returns its proof tree if it is an opetope, or raises an exception otherwise.

Here, we construct the proof tree of \(\mathsf{Y}_{\mathbf{2}} \circ_{[[*]]} \mathsf{Y}_{\mathbf{0}}\)

from opetopy.UnnamedOpetope import address, ProofTree

p = ProofTree({
    address([], 2): {
        address([], 1): {
            address('*'): {}  # {} represents the point
        },
        address(['*']): {
            address('*'): {}
        }
    },
    address([['*']]): {
        None: {}  # indicates a degeneracy
    }})

print(p)
print()
print(p.eval())

Here, we try to construct the proof tree of the invalid \(\mathsf{Y}_{\mathbf{1}} \circ_{[[***]]} \mathsf{Y}_{\mathbf{1}}\)

from UnnamedOpetope import address, ProofTree

ProofTree({
    address([], 2): {
        address([], 1): {
            address('*'): {}
        }
    },
    address([['*', '*', '*']]): {
        address([], 1): {
            address('*'): {}
        }
    }})

which raises an exception.

Documentation

Module author: Cédric HT

class opetopy.UnnamedOpetope.Address(dim: int)

The \(0\)-address \(*\) is construced as:

Address.epsilon(0)

More generally, the empty address is construced as:

Address.epsilon(n)

Recall that an \(n\)-address is by definition a sequence of \((n-1)\)-addresses. To append an \((n-1)\)-address to a \(n\)-address, use the Address.__add__() method. For instance, the following yields the \(1\)-address \([**]\):

Address.epsilon(1) + Address.epsilon(0) + Address.epsilon(0)

Given two \(n\)-addresses, it is possible to concatenate them using the Address.__mul__() method. Following up on the previous examples, the following expression yields the address \([****]\):

x = Address.epsilon(1) + Address.epsilon(0) + Address.epsilon(0)
x * x

__add__(other) → opetopy.UnnamedOpetope.Address

Adds the \((n-1)\)-address other at the end of the sequence of \((n-1)\)-addresses that make up the \(n\)-address self.

Warning:This is not concatenation (see Address.__mul__()).

__eq__(other) → bool

Compares two addresses. Two addresses are equal if they have the same dimension and the same underlying list of addresses.

__hash__()

Return hash(self).

__init__(dim: int) → None

Creates an empty address of dimension dim \(\geq 0\).

__lt__(other: opetopy.UnnamedOpetope.Address) → bool

Compares two addresses with respect to the lexicographical order.

__mul__(other: opetopy.UnnamedOpetope.Address) → opetopy.UnnamedOpetope.Address

Concatenates two \(n\)-addresses by concatenating the underlying lists of \((n-1)\)-addresses.

__repr__() → str

Return repr(self).

__str__() → str

Converts an address to a human readable string. The \(0\)-dimensional empty address is represented by the symbol *.

__weakref__

list of weak references to the object (if defined)

edgeDecomposition() → Tuple[opetopy.UnnamedOpetope.Address, opetopy.UnnamedOpetope.Address]

If the current address is of the form \([p[q]]\) (or equivalently, not an epsilon address), returns the tuple \(([p], [q])\).

static epsilon(dim: int) → opetopy.UnnamedOpetope.Address

Creates an empty address of dimension dim \(\geq 0\). Internally just calls Address.__init__().

static fromList(l: List[Any], dim: int) → opetopy.UnnamedOpetope.Address

Recursibely create an address of dimension dim from a list of lists that themselves represent addresses. The empty address is represented by [], and '*' represents the \(0\)-dimensional empty address.

static fromListOfAddresses(l: List[Address]) → opetopy.UnnamedOpetope.Address

Creates an address from a non empty list of addresses.

isEpsilon() → bool

Simply tells wither the current address is of the form \([]\).

shift(n: int = 1) → opetopy.UnnamedOpetope.Address

Returns the curent address shifted by \(n\) dimensions.

Example:

\([[][*]]\) .shift(2) is \([[[[][*]]]]\)

static substitution(a: opetopy.UnnamedOpetope.Address, b: opetopy.UnnamedOpetope.Address, c: opetopy.UnnamedOpetope.Address) → opetopy.UnnamedOpetope.Address

If the underlying sequence of b is a prefix of that of a, then replaces this prefix by the underlying sequence of c.

Example:

substitution( \([[*][**]]\) , \([[*]]\) , \([[][]]\) ) is \([[][][**]]\)

toTex() → str

Converts the address to TeX code.

opetopy.UnnamedOpetope.Arrow() → opetopy.UnnamedOpetope.RuleInstance

Returns the proof tree of the arrow.

class opetopy.UnnamedOpetope.Context(dim: int)

A \((n+1)\)-context can be seen as a partial injective function from the set \(\mathbb{A}_n\) of \(n\)-addresses to the set \(\mathbb{A}_{n-1}\) of \((n-1)\)-addresses.

__add__(other: Tuple[opetopy.UnnamedOpetope.Address, opetopy.UnnamedOpetope.Address]) → opetopy.UnnamedOpetope.Context

Adds a tuple of the form (math:n-address, \((n-1)\)-address) to the \((n+1)\)-context self.

__call__(addr: opetopy.UnnamedOpetope.Address) → opetopy.UnnamedOpetope.Address

If self is an (n+1)-context, returns the node \((n-1)\)-address associated to the given leaf \(n\)-address addr. Raises an exception if not defined.

__eq__(other) → bool

Tests equality between two contexts. Two contexts are equal if they have the same dimension and if the partial mapping \(\mathbb{A}_n \longrightarrow \mathbb{A}_{n-1}\) they represent are (extentionally) equal.

__init__(dim: int) → None

Creates an empty context of dimension \(\geq 0\).

__ne__(other) → bool

Return self!=value.

__next_in_mro__

alias of builtins.object

__repr__() → str

Return repr(self).

__str__() → str

Converts a context to a human readable string.

__sub__(addr: opetopy.UnnamedOpetope.Address) → opetopy.UnnamedOpetope.Context

Removes a address addr from the domain of definition of the context.

__weakref__

list of weak references to the object (if defined)

_gorg

alias of Context

definedOnLeaf(addr: opetopy.UnnamedOpetope.Address) → bool

Returns wether the context is defined on address addr.

leaves() → Set[opetopy.UnnamedOpetope.Address]

Returns the set of addresses on which the context is defined.

class opetopy.UnnamedOpetope.Degen(p: opetopy.UnnamedOpetope.RuleInstance)

A class representing an instance of the degen rule in a proof tree.

__init__(p: opetopy.UnnamedOpetope.RuleInstance) → None

Creates an instance of the degen rule and plugs proof tree p on the unique premise.

__repr__()

Return repr(self).

__str__()

Return str(self).

_toTex() → str

Converts the proof tree in TeX code. This method should not be called directly, use UnnamedOpetope.RuleInstance.toTex() instead.

eval() → opetopy.UnnamedOpetope.Sequent

Evaluates this instance of degen by first evaluating its premise, and then applying UnnamedOpetope.degen() on the resulting sequent.

class opetopy.UnnamedOpetope.Graft(p1: opetopy.UnnamedOpetope.RuleInstance, p2: opetopy.UnnamedOpetope.RuleInstance, addr: opetopy.UnnamedOpetope.Address)

A class representing an instance of the graft rule in a proof tree.

__init__(p1: opetopy.UnnamedOpetope.RuleInstance, p2: opetopy.UnnamedOpetope.RuleInstance, addr: opetopy.UnnamedOpetope.Address) → None

Creates an instance of the graft rule at address addr, and plugs proof tree p1 on the first premise, and p2 on the second. Recall that the opetope described in the second premise will be impropely grafted on that of the first. See UnnamedOpetope.graft().

__repr__()

Return repr(self).

__str__()

Return str(self).

_toTex() → str

Converts the proof tree in TeX code. This method should not be called directly, use UnnamedOpetope.RuleInstance.toTex() instead.

eval() → opetopy.UnnamedOpetope.Sequent

Evaluates this instance of graft by first evaluating its premises, and then applying UnnamedOpetope.graft() at address self.addr on the resulting sequents.

opetopy.UnnamedOpetope.OpetopicInteger(n: int) → opetopy.UnnamedOpetope.RuleInstance

Returns the sequent nth opetopic integer.

opetopy.UnnamedOpetope.OpetopicTree(tree: Optional[List[Any]]) → opetopy.UnnamedOpetope.RuleInstance

Returns the proof tree of the \(3\)-opetope corresponding to a tree. The tree is expressed as a recursive list. For instance, [None, [[None], None], None, None] corresponds to \(\mathsf{Y}_{\mathbf{4}} \circ_{[[*]]} \left( \mathsf{Y}_{\mathbf{2}} \circ_{[]} \mathsf{Y}_{\mathbf{1}} \right)\) while None corresponds to the degenerate opetope at the arrow.

class opetopy.UnnamedOpetope.Point

A class representing an instance of the point rule in a proof tree.

__repr__()

Return repr(self).

__str__()

Return str(self).

_toTex() → str

Converts the proof tree in TeX code. This method should not be called directly, use UnnamedOpetope.RuleInstance.toTex() instead.

eval() → opetopy.UnnamedOpetope.Sequent

Evaluates the proof tree, in this cases returns the point sequent by calling UnnamedOpetope.point().

class opetopy.UnnamedOpetope.Preopetope(dim: int)

Main class of the module.

__add__(t: Tuple[opetopy.UnnamedOpetope.Address, Preopetope]) → opetopy.UnnamedOpetope.Preopetope

Adds a (\((n-1)\)-address, \((n-1)\)-preopetope) tuple t to the non degenerate self \(n\)-preopetope. The \((n-1)\)-address must not be present.

__eq__(other)

Tests equality between two preopetopes. Two preopetopes are equal if they have the same dimension, and if either

• they are both degenerate on the same preopetope;
• they are both non degenerate, have the same (address, preopetope) tuples.

__init__(dim: int) → None

Inits an invalid preopetope of dimension dim. This method should not be called directly.

__repr__() → str

Return repr(self).

__str__() → str

Converts a preopetope to a human readable string. The \((-1)\)-preopetope is represented by "∅", the \(0\)-preopetope by "⧫", and the unique \(1\)-preopetope by "■".

__sub__(addr: opetopy.UnnamedOpetope.Address) → opetopy.UnnamedOpetope.Preopetope

Removes source at address addr.

__weakref__

list of weak references to the object (if defined)

static degenerate(q: opetopy.UnnamedOpetope.Preopetope) → opetopy.UnnamedOpetope.Preopetope

Constructs the degenerate preopetope at q.

static empty() → opetopy.UnnamedOpetope.Preopetope

Constructs the unique \((-1)\)-preopetope.

static fromDictOfPreopetopes(d: Dict[opetopy.UnnamedOpetope.Address, Preopetope]) → opetopy.UnnamedOpetope.Preopetope

Creates a non degenerate preopetope from a dict of preopetopes indexed by their addresses.

static grafting(p: opetopy.UnnamedOpetope.Preopetope, addr: opetopy.UnnamedOpetope.Address, q: opetopy.UnnamedOpetope.Preopetope) → opetopy.UnnamedOpetope.Preopetope

Grafts the \(n\)-preopetope q on the \(n\)-preopetope p at address addr. For improper grafting, see UnnamedOpetope.Preopetope.improperGrafting()

static improperGrafting(p: opetopy.UnnamedOpetope.Preopetope, addr: opetopy.UnnamedOpetope.Address, q: opetopy.UnnamedOpetope.Preopetope)

Performs the improper grafting of the \((n-1)\)-preopetope q on the \(n\)-preopetope p at address addr. For proper grafting, see UnnamedOpetope.Preopetope.grafting()

leafAddresses() → Set[opetopy.UnnamedOpetope.Address]

Returnst the set of leaf addresses of the preopetope.

nodeAddresses() → Set[opetopy.UnnamedOpetope.Address]

Returns the set of node addresses of the preopetope.

static point() → opetopy.UnnamedOpetope.Preopetope

Constructs the unique \(0\)-preopetope.

static substitution(p: opetopy.UnnamedOpetope.Preopetope, addr: opetopy.UnnamedOpetope.Address, ctx: opetopy.UnnamedOpetope.Context, q: opetopy.UnnamedOpetope.Preopetope)

In the \(n\)-preopetope p, substitute the source at address addr by the \((n-1)\)-preopetope q. The context ctx must be defined on all leaves of q (see UnnamedOpetope.Context.__call__()).

toDict() → Dict[Optional[opetopy.UnnamedOpetope.Address], Dict]

Transforms the current preopetope into a dict.

toTex() → str

Converts the preopetope to TeX code.

opetopy.UnnamedOpetope.ProofTree(p: Dict[Optional[opetopy.UnnamedOpetope.Address], Dict]) → opetopy.UnnamedOpetope.RuleInstance

Returns the proof tree of a preopetope described as a dict, or raises a common.DerivationError if the preopetope is not an opetope. For T the type of the argument, T is a dict mapping UnnamedOpetope.Address or None to instances of T. For example,

{
    address([], 1): {
        address('*'): {}
    },
    address(['*']): {
        address('*'): {}
    },
    address(['*', '*']): {
        address('*'): {}
    }
}

corresponds to the opetopic integer \(\mathbf{3}\), while

{
    None: {
        address('*'): {}
    }
}

is the \(3\)-opetope degenerate at the arrow (the None indicates a degeneracy).

class opetopy.UnnamedOpetope.RuleInstance

A rule instance of system \(\textbf{Opt${}^?$}\).

eval() → opetopy.UnnamedOpetope.Sequent

Pure virtual method evaluating a proof tree and returning the final conclusion sequent, or raising an exception if the proof is invalid.

class opetopy.UnnamedOpetope.Sequent(ctx: opetopy.UnnamedOpetope.Context, s: opetopy.UnnamedOpetope.Preopetope, t: opetopy.UnnamedOpetope.Preopetope)

A sequent is a triple consisting of an \(n\)-context, a source \(n\)-preopetope, and a target \((n-1)\)-preopetope.

__eq__(other) → bool

Return self==value.

__init__(ctx: opetopy.UnnamedOpetope.Context, s: opetopy.UnnamedOpetope.Preopetope, t: opetopy.UnnamedOpetope.Preopetope) → None

Creates a sequent from an \(n\)-context ctx, an \(n\)-preopetope s, and an \((n-1)\)-preopetope t.

__ne__(other) → bool

Return self!=value.

__repr__() → str

Return repr(self).

__str__() → str

Converts a sequent to a human readable string.

__weakref__

list of weak references to the object (if defined)

class opetopy.UnnamedOpetope.Shift(p: opetopy.UnnamedOpetope.RuleInstance)

A class representing an instance of the shift rule in a proof tree.

__init__(p: opetopy.UnnamedOpetope.RuleInstance) → None

Creates an instance of the shift rule and plugs proof tree p on the unique premise.

__repr__()

Return repr(self).

__str__()

Return str(self).

_toTex() → str

Converts the proof tree in TeX code. This method should not be called directly, use UnnamedOpetope.RuleInstance.toTex() instead.

eval() → opetopy.UnnamedOpetope.Sequent

Evaluates this instance of shift by first evaluating its premise, and then applying UnnamedOpetope.shift() on the resulting sequent.

opetopy.UnnamedOpetope.address(lst: Union[List[Any], str], dim: Optional[int] = None) → opetopy.UnnamedOpetope.Address

Similar to Address.fromList(), except the name is shorter, and the dimension is inferred if possible. Otherwise, an exception is thrown. Here are some examples:

>>> address('*')
Address(*, 0)

>>> address([['*'], [], ['*', '*']])
Address([[*][][**]], 2)

opetopy.UnnamedOpetope.degen(seq: opetopy.UnnamedOpetope.Sequent) → opetopy.UnnamedOpetope.Sequent

The \(\textbf{Opt${}^?$}\) \(\texttt{degen}\) rule. From an \(n\)-opetope \(\omega\), creates the degenerate \((n+2)\)-opetope \(\lbrace \lbrace \omega\).

opetopy.UnnamedOpetope.graft(seq1: opetopy.UnnamedOpetope.Sequent, seq2: opetopy.UnnamedOpetope.Sequent, addr: opetopy.UnnamedOpetope.Address) → opetopy.UnnamedOpetope.Sequent

The \(\textbf{Opt${}^?$}\) \(\texttt{graft}\) rule. From an \(n\)-opetope \(\omega\) (in sequent seq1), an \((n-1)\)-opetope \(\psi\) (in sequent seq2), and a leaf of \(\omega\), creates the opetope \(\omega \circ_{\mathrm{addr}} \mathsf{Y}_{\psi}\).

opetopy.UnnamedOpetope.point() → opetopy.UnnamedOpetope.Sequent

The \(\textbf{Opt${}^?$}\) \(\texttt{point}\) rule. Create the unique \(0\)-opetope with no premises.

opetopy.UnnamedOpetope.shift(seq: opetopy.UnnamedOpetope.Sequent) → opetopy.UnnamedOpetope.Sequent

The \(\textbf{Opt${}^?$}\) \(\texttt{shift}\) rule. From an \(n\)-opetope \(\omega\), creates the globular \((n+1)\)-opetope \(\lbrace []: \omega\).