Named Opetopes

Examples

The point

from opetopy.NamedOpetope import Point

pt = Point("x")
print(pt.eval())

A classic

from opetopy.NamedOpetope import Graft, Point, Shift

beta = Shift(Graft(
    Shift(Point("c"), "h"),
    Shift(Point("a"), "i"),
    "c"),
    "β")
alpha = Shift(Graft(
    Shift(Point("b"), "g"),
    Shift(Point("a"), "f"),
    "b"),
    "α")
classic = Shift(Graft(beta, alpha, "i"), "A")

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

Documentation

Module author: Cédric HT

opetopy.NamedOpetope.Arrow(pointName: str = 'a', arrowName: str = 'f') → opetopy.NamedOpetope.RuleInstance

Returns the proof tree of the arrow, with cell names as specified in the arguments.

class opetopy.NamedOpetope.Context

A context is a set of tyings (see NamedOpetope.Typing).

__add__(typing: opetopy.NamedOpetope.Typing) → opetopy.NamedOpetope.Context

Adds a variable typing to a deep copy of the context context, if the typed variable isn’t already typed in the context.

__and__(other) → opetopy.NamedOpetope.Context

Returns the intersection of two contexts, i.e. the set of typings of the first context whose typed variable is in the second

__contains__(var) → bool

Tests wether the variable var is typed in this context.

__getitem__(name: str) → opetopy.NamedOpetope.Variable

Returns the varible term in current context whose name is name.

__next_in_mro__

alias of builtins.object

__or__(other)

Returns the union of two compatible contexts.

__repr__() → str

Return repr(self).

__str__() → str

Return str(self).

_gorg

alias of Context

graftTuples() → Set[Tuple[opetopy.NamedOpetope.Variable, opetopy.NamedOpetope.Variable]]

Returns all tuples (b, a) for \(b \leftarrow a (\ldots)\) a grafting occurring in a term in a type in the context.

See:NamedOpetope.Term.graftTuples() See:NamedOpetopicSet.repres()

source(var: opetopy.NamedOpetope.Variable, k: int = 1) → opetopy.NamedOpetope.Term

Returns the :mathm``k``-source of a variable.

toTex() → str

Converts the type to TeX code.

typeOf(var: opetopy.NamedOpetope.Variable) → opetopy.NamedOpetope.Type

Returns the type of a variable.

variables() → Set[opetopy.NamedOpetope.Variable]

Return the set of all variables typed in the context.

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

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

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

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

__repr__() → str

Return repr(self).

__str__() → str

Return str(self).

_toTex() → str

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

eval() → opetopy.NamedOpetope.Sequent

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

class opetopy.NamedOpetope.DegenShift(p: opetopy.NamedOpetope.RuleInstance, name: str)

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

__init__(p: opetopy.NamedOpetope.RuleInstance, name: str) → None

Initialize self. See help(type(self)) for accurate signature.

__repr__() → str

Return repr(self).

__str__() → str

Return str(self).

_toTex() → str

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

eval() → opetopy.NamedOpetope.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.NamedOpetope.EquationalTheory

An equational theory (among variables), is here represented as a partition of a subset of the set of all variables. Is is thus a list of sets of variables. (set of sets isn’t possible as python set isn’t hashable)

__add__(eq: Tuple[opetopy.NamedOpetope.Variable, opetopy.NamedOpetope.Variable]) → opetopy.NamedOpetope.EquationalTheory

Adds an equality (represented by a tuple of two NamedOpetope.Variable) to the theory.

__init__() → None

Initialize self. See help(type(self)) for accurate signature.

__or__(other: opetopy.NamedOpetope.EquationalTheory) → opetopy.NamedOpetope.EquationalTheory

Returns the union of two equational theories

__repr__() → str

Return repr(self).

__str__() → str

Return str(self).

__weakref__

list of weak references to the object (if defined)

_index(a: opetopy.NamedOpetope.Variable) → int

Returns the index (in NamedOpetope.EquationalTheory.classes) of the class of the variable a, or -1 of the class doesn’t exist.

classOf(a: opetopy.NamedOpetope.Variable) → Set[opetopy.NamedOpetope.Variable]

Returns the class of a variable.

equal(a: opetopy.NamedOpetope.Variable, b: opetopy.NamedOpetope.Variable) → bool

Tells wether variables (NamedOpetope.Variable) a and b are equal modulo the equational theory.

isIn(var: opetopy.NamedOpetope.Variable, term: opetopy.NamedOpetope.Term) → bool

Tells wether a variable is in a term modulo the equational theory of the sequent.

See:NamedOpetope.Term.__contains__().

class opetopy.NamedOpetope.Graft(p1: opetopy.NamedOpetope.RuleInstance, p2: opetopy.NamedOpetope.RuleInstance, a: str)

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

__init__(p1: opetopy.NamedOpetope.RuleInstance, p2: opetopy.NamedOpetope.RuleInstance, a: str) → None

Creates an instance of the graft rule at variable a, and plugs proof tree p1 on the first premise, and p2 on the second.

See:NamedOpetope.graft().

__repr__() → str

Return repr(self).

__str__() → str

Return str(self).

_toTex() → str

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

eval() → opetopy.NamedOpetope.Sequent

Evaluates this instance of graft by first evaluating its premises, and then applying NamedOpetope.graft() at variable self.variableName on the resulting sequents.

class opetopy.NamedOpetope.OCMT(theory: opetopy.NamedOpetope.EquationalTheory, context: opetopy.NamedOpetope.Context)

Opetopic context modulo theory. Basically the same as a NamedOpetope.Sequent, without the typing.

__init__(theory: opetopy.NamedOpetope.EquationalTheory, context: opetopy.NamedOpetope.Context) → None

Initialize self. See help(type(self)) for accurate signature.

__repr__() → str

Return repr(self).

__str__() → str

Return str(self).

__weakref__

list of weak references to the object (if defined)

equal(t: opetopy.NamedOpetope.Term, u: opetopy.NamedOpetope.Term) → bool

Tells wether two terms t and u are equal modulo the equational theory.

See:Similar method for variables only: NamedOpetope.EquationalTheory.equal()

isIn(var: opetopy.NamedOpetope.Variable, term: opetopy.NamedOpetope.Term) → bool

Tells wether a variable is in a term modulo the equational theory of the sequent.

See:NamedOpetope.EquationalTheory.isIn() See:NamedOpetope.Term.__contains__()

source(var: opetopy.NamedOpetope.Variable, k: int = 1) → opetopy.NamedOpetope.Term

Returns the :mathm``k``-source of a variable.

See:NamedOpetope.Context.source()

target(var: opetopy.NamedOpetope.Variable, k: int = 1) → opetopy.NamedOpetope.Variable

Returns the \(k\) target of a variable.

typeOf(var: opetopy.NamedOpetope.Variable) → opetopy.NamedOpetope.Type

Returns the type of a variable.

See:NamedOpetope.Context.typeOf()

opetopy.NamedOpetope.OpetopicInteger(n: int, pointName: str = 'a', arrowName: str = 'f', cellName: str = 'A') → opetopy.NamedOpetope.RuleInstance

Returns the proof tree of the \(n\)-th opetopic integer.

• if n is 0, then the unique point is named pointName (default a), and the unique \(2\)-cell is named cellName (default A).
• otherwise, the points are named a_1, a_2, … a_n-1 (with added braces if the index exceeds 10, so that it is \(\TeX\) friendly), arrows f_1, … f_n. Those names can be changed by specifying the pointName and arrowName arguments. The unique \(2\)-cell is named cellName (default A).

class opetopy.NamedOpetope.Point(name: str)

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

__init__(name: str) → None

Initialize self. See help(type(self)) for accurate signature.

__repr__() → str

Return repr(self).

__str__() → str

Return str(self).

_toTex() → str

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

eval() → opetopy.NamedOpetope.Sequent

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

class opetopy.NamedOpetope.RuleInstance

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

eval() → opetopy.NamedOpetope.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.NamedOpetope.Sequent(theory: opetopy.NamedOpetope.EquationalTheory, context: opetopy.NamedOpetope.Context, typing: opetopy.NamedOpetope.Typing)

A sequent consists of an equational theory (NamedOpetope.EquationalTheory), a context (NamedOpetope.Context), and a typing (NamedOpetope.Typing).

__init__(theory: opetopy.NamedOpetope.EquationalTheory, context: opetopy.NamedOpetope.Context, typing: opetopy.NamedOpetope.Typing) → None

Initialize self. See help(type(self)) for accurate signature.

__repr__() → str

Return repr(self).

__str__() → str

Return str(self).

graft(t: opetopy.NamedOpetope.Term, x: opetopy.NamedOpetope.Variable, u: opetopy.NamedOpetope.Term) → opetopy.NamedOpetope.Term

Grafts term (NamedOpetope.Term) u on term t via variable (NamedOpetope.Variable) x. In other words, computes \(t(x \leftarrow u)\).

substitute(u: opetopy.NamedOpetope.Term, s: opetopy.NamedOpetope.Term, a: opetopy.NamedOpetope.Variable) → Tuple[opetopy.NamedOpetope.Term, Optional[Tuple[opetopy.NamedOpetope.Variable, opetopy.NamedOpetope.Variable]]]

Substitute term (NamedOpetope.Term) s for variable (NamedOpetope.Variable) a in term u. In other words, computes \(u[s/a]\).

Returns a tuple containing

1. the resulting substitution
2. an new equality to add to the equational theory, or None

typing = None

This variable specifies if contexts should be displayed in NamedOpetope.Sequent.toTex()

class opetopy.NamedOpetope.Shift(p: opetopy.NamedOpetope.RuleInstance, name: str)

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

__init__(p: opetopy.NamedOpetope.RuleInstance, name: str) → None

Initialize self. See help(type(self)) for accurate signature.

__repr__() → str

Return repr(self).

__str__() → str

Return str(self).

_toTex() → str

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

eval() → opetopy.NamedOpetope.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.NamedOpetope.Term(var: Optional[opetopy.NamedOpetope.Variable] = None, degen: bool = False)

An \(n\)-term is represented as follows:

• If it is degenerate, then the boolean attribute NamedOpetope.Term.degenerate is set to True, and NamedOpetope.Term.variable is set to the variable name of which the current term is the degeneracy.
• If it is non degenerate, then the boolean attribute NamedOpetope.Term.degenerate is set to False, NamedOpetope.Term.variable is set to the variable name of the root node, and this class is otherwise used as a dict mapping \((n-1)\)-variables in the source to other \(n\)-terms.

__contains__(var) → bool

Checks if a variable is in the term.

If the term is degenerate, always return False. Otherwise, assume the term has dimension \(n\).

• If the variable has dimension \((n-1)\), then it checks against all keys in the underlying dict and if not found, calls the method recursively on all values of the underlying dict (which by construction are also \(n\)-terms).
• If the variable has \(n\), then it compares it to the root node (NamedOpetope.Term.variable), and if not equal, calls the method recursively on all values of the underlying dict (which by construction are also \(n\)-terms).

__eq__(other) → bool

Tests if two terms are syntactically equal.

__init__(var: Optional[opetopy.NamedOpetope.Variable] = None, degen: bool = False) → None

Creates a term from a NamedOpetope.Variable var. If it is None (default), then this term represents the unique \((-1)\)-term.

__ne__(other) → bool

Return self!=value.

__next_in_mro__

alias of builtins.object

__repr__() → str

Return repr(self).

__str__() → str

Return str(self).

__weakref__

list of weak references to the object (if defined)

_gorg

alias of Term

dimension

Returns the dimension of the term. If its NamedOpetope.Term.variable is None, then it is \(-1\) by convention. If it is degenerate, then it is the dimension of NamedOpetope.Term.variable \(+1\), otherwise just the dimension of NamedOpetope.Term.variable.

graftTuples() → Set[Tuple[opetopy.NamedOpetope.Variable, opetopy.NamedOpetope.Variable]]

This helper function constructs the set of tuples (b, a) for all variables a and b such that the expression \(b \leftarrow a (\ldots)\) occurs in the term.

isVariable() → bool

Tells wether this term is in fact just a variable.

toTex() → str

Converts the term to TeX code.

variables(k) → Set[opetopy.NamedOpetope.Variable]

Returns the set of all \(k\) variables contained in the term. Note that degenerate terms don’t containe any variables.

See:NamedOpetope.Term.__contains__()

class opetopy.NamedOpetope.Type(terms: List[opetopy.NamedOpetope.Term])

An \(n\)-type is a sequence of \((n+1)\) terms of dimension \((n-1), (n-2), \ldots, -1\).

__contains__(var) → bool

Checks wether a given variable appears in at least one term of the type.

__init__(terms: List[opetopy.NamedOpetope.Term]) → None

Creates a new type from a list of term. The dimension is inferred from the length of the list, and the terms are checked to have the correct dimension.

If the list has length \((n+1)\), then the type’s dimension will be \(n\), and the dimension of the \(i\) th term in the list must be \(n - i - 1\) (recall that Python index start at \(0\), whence the \(-1\) correction factor).

__repr__() → str

Return repr(self).

__str__() → str

Return str(self).

__weakref__

list of weak references to the object (if defined)

toTex() → str

Converts the type to TeX code.

variables(k: int) → Set[opetopy.NamedOpetope.Variable]

Returns the set of all \(k\) variables contained in the terms of the type. Note that degenerate terms don’t containe any variables.

See:NamedOpetope.Term.__contains__() See:NamedOpetope.Term.variables()

class opetopy.NamedOpetope.Typing(term, type)

A typing is simply an \(n\)-term (NamedOpetope.Term)

together with an \(n\)-type (NamedOpetope.Type).

__hash__()

Return hash(self).

__init__(term, type) → None

Initialize self. See help(type(self)) for accurate signature.

__repr__() → str

Return repr(self).

__str__() → str

Return str(self).

__weakref__

list of weak references to the object (if defined)

class opetopy.NamedOpetope.Variable(name: str, dim: int)

A variable is just a string representing its name, annotated by an integer representing its dimension.

__eq__(other) → bool

Tests syntactic equality between two variables. Two variables are equal if they have the same dimension and the same name.

__hash__()

Return a hash of the variable. This is for Python purposes.

__init__(name: str, dim: int) → None

Initialize self. See help(type(self)) for accurate signature.

__ne__(other) → bool

Return self!=value.

__repr__() → str

Return repr(self).

__str__() → str

Return str(self).

__weakref__

list of weak references to the object (if defined)

toTex() → str

Returns the string representation of the variable, which is really just the variable name.

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

The \(\textbf{Opt${}^!$}\) \(\texttt{degen}\) rule. Takes a sequent typing a variable and produces a new sequent typing the degeneracy at that variable.

opetopy.NamedOpetope.degenshift(seq: opetopy.NamedOpetope.Sequent, name: str) → opetopy.NamedOpetope.Sequent

The \(\textbf{Opt${}^!$}\) \(\texttt{degen-shift}\) rule. Applies the degen and the shift rule consecutively.

opetopy.NamedOpetope.graft(seqt: opetopy.NamedOpetope.Sequent, seqx: opetopy.NamedOpetope.Sequent, name: str) → opetopy.NamedOpetope.Sequent

The \(\textbf{Opt${}^!$}\) \(\texttt{graft}\) rule. Takes the following arguments:

1. seqt typing an \(n\) term \(t\)
2. seqx second typing an \(n\) variable \(x\)
3. an \((n-1)\) variable a onto which to operate the grafting, specified by its name name

such that the two sequents are compatible, and the intersection of their context is essentially the context typing a and its variables. It then produces the \(n\) term \(t(a \leftarrow x)\).

The way the intersection condition is checked is by verifying that the only variables typed in both contexts (modulo both theories) are those appearing in the type of a or of course a itself.

opetopy.NamedOpetope.point(name: str) → opetopy.NamedOpetope.Sequent

The \(\textbf{Opt${}^!$}\) \(\texttt{point}\) rule. Introduces a \(0\)-variable with name x.

opetopy.NamedOpetope.shift(seq: opetopy.NamedOpetope.Sequent, name: str) → opetopy.NamedOpetope.Sequent

The \(\textbf{Opt${}^!$}\) \(\texttt{shift}\) rule. Takes a sequent seq typing a term t and introduces a new variable x having t as \(1\)-source.