Sammy

This article is not detailed enough and needs to be expanded. Please help us by adding some more information.

Sammy

Paradigm(s)	declarative
Designed by	Noson Yanofsky
Appeared in	2013
Type system	strong, static, implicit
Computational class	Unknown
Reference implementation	Unimplemented
Influenced by	Hagino CPL

Sammy is a language for constructing categories, particularly objects of the wikipedia:category of small categories Cat. It was introduced to measure the wikipedia:Kolmogorov complexity of constructions in category theory.

Syntax

Sammy is only specified up to abstract syntax. A Sammy program is a labeled sequence of assignments, unconditional jumps, and conditional jumps. An assignment attaches global names to a construction made out of other global names and builtin operations. A jump makes at most one comparison, asking whether two natural transformations are equivalent, and if successful, control is transferred to a fixed program label.

The following concrete syntax is based on the original presentation in (Yanofsky, 2013). A name is either constant or mutable. A name refers to an object, arrow, category, functor, or natural transformation; this classification is the entirety of the type system. The constant names are the following categories:

• 0
• 1
• 2
• Cat

And the following functors:

• s : 1 → 2
• t : 1 → 2
• ! : 0 → 1
• ! : 0 → 2
• ! : 0 → Cat
• ! : Cat → 1
• ! : 2 → 1

An assignment consists of a tuple of target names, an operation, and a tuple of source names. All assignments must be correctly typed. In the following listing, type annotations `obj`, `arr`, `cat`, `func`, and `nt` are given for the reader's benefit but are not part of the concrete syntax.

C :cat = Source(F :func)
D :cat = Target(F :func)
Id_C :func = Ident(C :cat)
C_op :[cat,func] = Op(C :[cat,func])
x :[obj,arr] = Pick(F_x :func)
F_x :func = Determine(x :[obj,arr])
alpha :nt = Hcomp(beta :[func,nt], gamma :[func,nt])
alpha :nt = Vcomp(beta :nt, gamma :nt)
C_D :cat = Pow(C :cat, D :cat)
R :func, alpha :nt = KanEx(G :func, F :func)
gamma :nt = KanInd(F :func, G :func, H: func, beta :nt)
C :cat, in_L :func, in_R :func = L :cat ⊔ R :cat
R :func, alpha :nt = KanLif(G :func, F :func)
F :func = Composable(C :cat)

The ⊔ operator is infix.

There are two forms of jump. A conditional jump compares two natural transformations for equivalence first:

If alpha :nt == beta :nt Goto L

An unconditional jump is merely a goto:

Goto L

Semantics

The semantics are straightforward constructions in Cat according to the rules of the Elementary Theory of the Category of Categories. If an operation fails due to type issues, then the construction is stuck.

Composition of natural transformations, or any other composition, is only valid when all types line up. Otherwise, as the reader may guess, it is stuck.

The operations Pick and Determine are polymorphic. A functor can only be Picked if its Source is 1 or 2; when Source is 1, its Pick is an object, when Source is 2, its Pick is an arrow, and otherwise Pick is stuck. Both objects and arrows can be Determined.

The KanEx operation produces the right wikipedia:Kan extension. Similarly, the KanLif operation produces the right Kan lifting. In the rare case where a Kan extension or lifting doesn't exist, these operations are stuck.

Idioms

The discrete ordinals are individually constructed from coproducts:

B = 1 ⊔ 1
3 = 1 ⊔ B
4 = B ⊔ B

The following program constructs the walking span (Yanofsky, 2013, p7):

S, in_L, in_R = 2 ⊔ 2
f = Hcomp(s, in_L)
g = Hcomp(s, in_R)
# XXX form the diagram d somehow?
R, alpha = KanEx(!, d)

A similar span constructs the additive monoid of natural numbers:

J = Pow(1, 2)
# XXX do the Kan extension to coequalize
R, alpha = KanEx(!, J)

Kolmogorov complexity

The main goal of Sammy is to study the function K : Cat → N which counts the size of the smallest program required to construct a category. As is typical for Kolmogorov complexity, this will not be easy because of a variant of wikipedia:Berry's paradox:

Theorem. K is not computable. In particular, as a functor, K is not constructible in Sammy. (Yanofsky, 2013)

We nonetheless have some nice results. Let K(C) ≈ K(D) when the absolute difference of K(C|D) and K(D|C) is bounded; intuitively, C can be transformed into D or vice versa by a bounded number of Sammy operations. Importantly:

Theorem. If categories C and D are equivalent then K(C) ≈ K(D). (Yanofsky, 2013)

That is, every wikipedia:equivalence of categories in Cat can be used to extend a Sammy program for either C or D with a constant number of additional instructions in order to witness that equivalence.

Complexity class

Sammy can encode primitive-recursive functionals and simulate a Turing machine. It is not known whether Turing machines can validate every Sammy program.

Additionally, the structure of Sammy validates the wikipedia:structured program theorem, suggesting that Sammy is complete for computable constructions over Cat.

Implementations

An abstract interpreter is available here containing most of the basics. It cannot explicitly compute Kan extensions. For example, it can count arrows of coproducts:

>>> print(sum(two, two)[0])
2 ⊔ 2 (6 arrows)
>>> print(sum(one, one, one, one)[0])
1 ⊔ 1 ⊔ 1 ⊔ 1 (4 arrows)

It can also explicitly compute elements of finite categories:

>>> print("the element selected by", s, "is", s.pick())
the element selected by s : 1 (1 arrows) → 2 (3 arrows) is <element 0 ∈ 2 (3 arrows)>

References

• "Kolmogorov Complexity of Categories", Yanofsky 2013
• "Counting Finite Categories", Cruttwell & Leblanc 2014, New Directions in Category Theory