TermBase

class discopy.closed.TermBase(name, dom, cod, **params)

Bases: Box, discopy.biclosed.TermBase

A term in the internal language of a closed category, i.e. a lambda term which need not be linear: this module implements closed markov categories by design, so a variable may be copied and discarded, i.e. occur any number of times.

A term is evaluated in a context, a list of distinct variables containing its free ones: the variables that do not occur in the term are discarded, the others are permuted into the order of its freevars, see weaken(). The context is freevars itself by default.

Note

Closed terms accept the left argument of their biclosed counterparts and ignore it: a closed category has one exponential, so an application x(f, left=True) is f(x) and an abstraction on the left is one on the right.

>>> X, Y = Ty("X"), Ty("Y")
>>> f, x = (X >> Y)("f"), X("x")
>>> assert x(f, left=True) == f(x)

Parameters:

• name (str)

• dom (Ty)

• cod (Ty)

compose(*others)

The composition of terms of function types: t.compose(u) for t : x >> y and u : y >> z is x(lambda v: u(t(v))), i.e. t is applied first, in the order of t >> u, which composes the diagrams that terms also are and keeps its name.

Parameters:

others (Term) – Terms of function types, the exponent of each being the base of the previous one.

Return type:

Term

Example

>>> X, Y, Z = map(Ty, "XYZ")
>>> t, u = (X >> Y)("t"), (Y >> Z)("u")
>>> print(t.compose(u))
X(lambda x: u(t(x)))

weaken(functor, context=None)

The structural morphism from the image of a context to that of the free variables of the term: it discards the variables that do not occur in the term and permutes the others into the order of freevars.

Parameters:

• functor (Functor) – The functor to evaluate the types.

• context – A list of distinct variables containing the free ones, the free variables themselves by default.

Return type:

Diagram

Example

>>> X, Y = Ty("X"), Ty("Y")
>>> x, y = Variable("x", X), Variable("y", Y)
>>> assert x.weaken(x.functor, [y, x])\
...     == Diagram.swap(Y, X) >> X @ Diagram.discard(Y)

share(functor, *contexts)

The structural morphism from the image of the free variables of the term to that of the concatenation of contexts, copying each variable once for each of the contexts it is in, i.e. how the subterms of a term share its free variables.

Parameters:

• functor (Functor) – The functor to evaluate the types.

• contexts (list[Variable]) – Lists of distinct free variables, one per subterm, each variable being in at least one of them.

Return type:

Diagram

Example

>>> X, Y = Ty("X"), Ty("Y")
>>> x, y = Variable("x", X), Variable("y", Y)
>>> term = Tuple(x, y, x)
>>> assert term.share(term.functor, [x], [y], [x])\
...     == Diagram.copy(X) @ Y >> X @ Diagram.swap(X, Y)

eval_unpacked(functor=None, context=None)

The evaluation of a term followed by the unpacking of its product codomain, overridden by Tuple so that binding a literal tuple never produces a Pack followed by an Unpack.

occurrences(variable)

The number of free occurrences of a variable in the term.

Parameters:

variable (Variable)

Return type:

int

substitute(substitution)

The term with the free variables of a substitution replaced.

Parameters:

substitution (Substitution)

Return type:

Term

classmethod from_biclosed(term)

Translate a biclosed term into a closed term, dropping planarity by collapsing left and right exponentials and applications.

Parameters:

term (Term) – The biclosed term to translate.

Return type:

Term

Note

This method is inherited by Constant, Variable, Application and Abstraction, i.e. every closed Term.

Example

>>> X, Y = biclosed.Ty("X"), biclosed.Ty("Y")
>>> g, x = (Y << X)("g"), X("x")
>>> print(TermBase.from_biclosed(g(x)))
g(x)