The GEB Manual
Table of Contents
 1 Links
 2 Getting Started
 3 Glossary
 4 Original Efforts
 5 Categorical Model
 6 Project Idioms and Conventions
 7 The Geb Model
 8 Extension Sets for Categories
 9 The GEB GUI
 10 Seqn Specification
 11 Bits (Boolean Circuit) Specification
 12 Polynomial Specification
 13 The Simply Typed Lambda Calculus model
 14 Mixins
 15 Geb Utilities
 16 Testing
[in package GEBDOCS/DOCS]
Welcome to the GEB project.
1 Links
Here is the official repository
and HTML documentation for the latest version.
Maintainers: please read the maintainers guide
1.1 code coverage
For test coverage it can be found at the following links:
CCL test coverage: current under maintenance
Note that due to #34 CCL tests are not currently displaying
I recommend reading the CCL code coverage version, as it has proper tags.
Currently they are manually generated, and thus for a more accurate assessment see GEBTEST:CODECOVERAGE
2 Getting Started
Welcome to the GEB Project!
2.1 installation
This project uses common lisp, so a few dependencies are needed to get around the codebase and start hacking. Namely:
Emacs along with one of the following:
2.2 loading
Now that we have an environment setup, we can load the project, this can be done in a few steps.
Open the
REPL
(sbcl (terminal),Mx
sly,Mx
swank)For the terminal, this is just calling the common lisp implementation from the terminal.
user@system:gebdirectory % sbcl
.For Emacs, this is simply calling either
Mx sly
orMx slime
if you are using either sly or slime
From Emacs: open
geb.asd
and pressCck
(slycompileandloadfile
, orswankcompileandloadfile
if you are using swank).
Now that we have the file open, we can now load the system by writing:
;; only necessary for the first time!
(ql:quickload :geb/documentation)
;; if you want to load it in the future
(asdf:loadsystem :geb/documentation)
;; if you want to load the codbase and run tests at the same time
(asdf:testsystem :geb/documentation)
;; if you want to run the tests once the system is loaded!
(gebtest:runtests)
2.3 Geb as a binary
[in package GEB.ENTRY]
The standard way to use geb currently is by loading the code into one's lisp environment
(ql:quickload :geb)
However, one may be interested in running geb in some sort of compilation process, that is why we also give out a binary for people to use
An example use of this binary is as follows
mariari@Gensokyo % ./geb.image i "foo.lisp" e "geb.lambda.main::*entry*" l p o "foo.pir"
mariari@Gensokyo % cat foo.pir
def entry x1 = {
(x1)
};%
mariari@Gensokyo % ./geb.image i "foo.lisp" e "geb.lambda.main::*entry*" l p
def *entry* x {
0
}
mariari@Gensokyo % ./geb.image h
i input string Input geb file location
e entrypoint string The function to run, should be fully qualified I.E. geb::mymain
l stlc boolean Use the simply typed lambda calculus frontend
o output string Save the output to a file rather than printing
v version boolean Prints the current version of the compiler
p vampir string Return a vampir expression
h ? help boolean The current help message
mariari@Gensokyo % ./geb.image v
0.3.2
starting from a file foo.lisp that has
any valid lambda form. Good examples can be found at the following section:
The Simply Typed Lambda Calculus model
with the term bound to some global variable
(inpackage :geb.lambda.main)
(defparameter *entry*
(lamb (list (coprod so1 so1))
(index 0)))
inside of it.
The command needs an entrypoint (e or entrypoint), as we are
simply call LOAD
on the given file, and need to know what to
translate.
from STLC
, we expect the form to be wrapped in the
GEB.LAMBDA.SPEC.TYPED which takes both the type and the value to
properly have enough context to evaluate.
It is advised to bind this to a parameter like in our example as e expects a symbol.
the l flag means that we are not expecting a geb term, but rather a lambda frontend term, this is to simply notify us to compile it as a lambda term rather than a geb term. In time this will go away
 [function] COMPILEDOWN &KEY VAMPIR STLC ENTRY (STREAM
*STANDARDOUTPUT*
)
3 Glossary

A closed type is a type that can not be extended dynamically. A good example of this kind of term is an ML ADT.
data Tree = Empty  Leaf Int  Node Tree Tree
In our lisp code we have a very similar convention:
(inpackage :geb.spec) (deftype substmorph () `(or substobj alias comp init terminal case pair distribute injectleft injectright projectleft projectright))
This type is closed, as only one of
GEB:SUBSTOBJ
,GEB:INJECTLEFT
,GEB:INJECTRIGHT
etc can form theGEB:SUBSTMORPH
type.The main benefit of this form is that we can be exhaustive over what can be found in
GEB:SUBSTMORPH
.(defun sohomobj (x z) (matchof substobj x (so0 so1) (so1 z) (alias (sohomobj (obj x) z)) ((coprod x y) (prod (sohomobj x z) (sohomobj y z))) ((prod x y) (sohomobj x (sohomobj y z)))))
If we forget a case, like
GEB:COPROD
it wanrs us with an non exhaustion warning.Meaning that if we update definitions this works well.
The main downside is that we can not extend the type after the fact, meaning that all interfaces on SOHOMOBJ must take the unaltered type. This is in stark contrast to open types. To find out more about the trade offs and usage in the codebase read the section Open Types versus Closed Types.

An open type is a type that can be extended by user code down the line. A good example of this in ML is the type class system found in Haskell.
In our code base, it is simple as creating a Common Lisp Object System (CLOS) term
(defclass <substobj> (directpointwisemixin) ())
and to create a child of it all we need to do is.
(defclass so0 (<substobj>) ())
Now any methods on
GEB:<SUBSTOBJ>
will coverGEB:SO0
(0
1
).
The main disadvantage of these is that exhaustion can not be checked, and thus the user has to know what methods to fill out. In a system with a bit more checks this is not a problem in practice. To find out more about the trade offs and usage in the codebase read the section Open Types versus Closed Types.
[glossaryterm] Common Lisp Object System (CLOS)
The object system found in CL. Has great features like a Meta Object Protocol that helps it facilitate extensions.
4 Original Efforts
Originally GEB started off as an Idris codebase written by the designer and creator of GEB, Terence Rokop, However further efforts spawned for even further formal verification by Artem Gureev. Due to this, we have plenty of code not in Common Lisp that ought to be a good read.
4.1 Geb's Idris Code
The Idris folder can be found in the gebidris folder provided in the codebase
At the time of this document, there is over 16k lines of Idris code written. This serves as the bulk of the POC that is GEB and is a treasure trove of interesting information surrounding category theory.
4.2 Geb's Agda Code
The Agda folder can be found in the gebagda folder provided in the codebase
The Agda codebase serves as a great place to view formally verified properties about the GEB project. Although Geb's Idris Code is written in a dependently typed language, it serves as reference example of GEB, while Geb's Agda Code serves as the mathematical formalism proving various conjectures about GEB
5 Categorical Model
Geb is organizing programming language concepts (and entities!) using category theory, originally developed by mathematicians, but very much alive in programming language theory. Let us look at a simple wellknown example: the category of sets and functions. It is the bread and butter example: sets $A,B,C,…$ play the role of objects, functions are arrows between objects $A—f→B$, and the latter compose as functions do, such that every path of matching functions $$A—f→B—g→C—h→D$$ composes to a corresponding composite function $$A—f;g;h→D$$ (or $h∘g∘f$ if you prefer) and we enjoy the luxury of not having to worry about the order in which we compose; for the sake of completeness, there are identify functions $A —\mathrm{id}_A→ A$ on each set $A$, serving as identities (which correspond to the composite of the empty path on an object). Sets and functions together form a category—based on function composition; thus, let's call this category sets'n'functions. This example, even “restricted” to finite sets'n'functions, will permeate through Geb.
One of the first lessons (in any introduction to category theory) about sets'n'functions is the characterization of products and disjoint sums of sets in terms of functions alone, i.e., without ever talking about elements of sets. Products and coproducts are the simplest examples of universal constructions. One of the first surprises follows suit when we generalize functions to partial functions, relations, or even multirelations: we obtain very different categories! For example, in the category sets'n'relations, the disjoint union of sets features as both a product and a coproduct, as a categorical construction.
Do not fear! The usual definition of products in terms of elements of sets are absolutely compatible with the universal construction in sets'n'functions. However we gain the possibility to compare the “result” of the universal constructions in sets'n'functions with the one in sets'n'relations (as both actually do have products).
for the purposes of Geb, many things can be expressed in analogy to the category of sets'n'functions; thus a solid understanding of the latter will be quite useful. In particular, we shall rely on the following universal constructions:
The construction of binary products $A × B$ of sets $A,B$, and the empty product $mathsf{1}$.
The construction of “function spaces” $B^A$ of sets $A,B$, called exponentials, i.e., collections of functions between pairs of sets.
The socalled currying of functions, $C^{(B^A)} cong C^{(A × B)}$, such that providing several arguments to a function can done either simultaneously, or in sequence.
The construction of sums (a.k.a. coproducts) $A + B$ of sets $A,B$, corresponding to forming disjoint unions of sets; the empty sum is $varnothing$.
Product, sums and exponentials are the (almost) complete tool chest for writing polynomial expressions, e.g., $$Ax^{sf 2} +x^{sf 1}  Dx^{sf 0}.$$ (We need these later to define “algebraic data types”.) In the above expression, we have sets instead of numbers/constants where $ mathsf{2} = lbrace 1, 2 rbrace$, $ mathsf{1} = lbrace 1 rbrace$, $ mathsf{0} = lbrace rbrace = varnothing$, and $A$ and $B$ are arbitrary (finite) sets. We are only missing a counterpart for the variable! Raising an arbitrary set to “the power” of a constant set happens to have a very natural counterpart: the central actor of the mostwell known fundamental result about categories, which generalizes Cayley's Theorem, i.e., the Yoneda embedding.
If you are familiar with the latter, buckle up and jump to Poly in Sets. Have a look at our streamlined account of The Yoneda Lemma if you are familiar with Cartesian closed categories, or take it slow and read up on the background in one of the classic or popular textbooks. Tastes tend to vary. However, Benjamin Pierce's Basic Category Theory for Computer Scientists deserves being pointed out as it is very amenable and covers the background we need in 60 short pages.
5.1 Morphisms
5.2 Objects
5.3 The Yoneda Lemma
5.4 Poly in Sets
6 Project Idioms and Conventions
The Geb Project is written in Common Lisp, which means the authors have a great choice in freedom in how the project is laid out and operates. In particular the style of Common Lisp here is a functional style with some OO idioms in the style of Smalltalk.
The subsections will outline many idioms that can be found throughout the codebase.
6.1 Spec Files, Main Files and Project Layout
[in package GEB.SPECS]
The codebase is split between many files. Each folder can be seen as
a different idea within geb itself! Thus the poly
has packages
revolving around polynomials, the geb
folder has packages regarding
the main types of geb Subst Obj and
Subst Morph, etc etc.
The general layout quirk of the codebase is that packages like
geb.package.spec
defines the specification for the base types for
any category we wish to model, and these reside in the specs
folder
not in the folder that talks about the packages of those types. This
is due to loading order issues, we thus load the specs
packages
before each of their surrounding packages, so that each package can
built off the last. Further, packages like geb.package.main
define
out most of the functionality of the package to be used by other
packages in geb.package
, then all of these are reexported out in the
geb.package
package
Further to make working with each package of an idea is easy, we have the main package of the folder (typically named the same as the folder name) reexport most important components so if one wants to work with the fully fledged versions of the package they can simply without having to import too many packages at once.
For example, the geb.poly.spec
defines out the types and data
structures of the Polynomial Types, this is then rexported
in geb.poly
, giving the module geb.poly
a convenient interface for
all functions that operate on geb.poly
.
6.2 Open Types versus Closed Types
closed type's and open type's both have their perspective tradeoff of openness versus exhaustiveness (see the linked articles for more on that). Due to this, they both have their own favorable applications. I would argue that a closed ADT type is great tool for looking at a function mathematically and treating the object as a whole rather than piecemeal. Whereas a more open extension is great for thinking about how a particular object/case behaves. They are different mindsets for different styles of code.
In the geb project, we have chosen to accept both styles, and allow both to coexist in the same setting. We have done this with a two part idiom.
(deftype substobj ()
`(or alias prod coprod so0 so1))
(defclass <substobj> (directpointwisemixin) ())
(defclass so0 (<substobj>) ...)
(defclass prod (<substobj>) ...)
The closed type is GEB:SUBSTOBJ
, filling and defining every structure
it knows about. This is a fixed idea that a programmer may statically
update and get exhaustive warnings about. Whereas GEB:<SUBSTOBJ>
is
the open interface for the type. Thus we can view GEB:<SUBSTOBJ>
as
the general idea of a GEB:SUBSTOBJ
. Before delving into how we combine
these methods, let us look at two other benefits given by GEB:<SUBSTOBJ>
We can put all the Mixins into the superclass to enforce that any type that extends it has the extended behaviors we wish. This is a great way to generically enhance the capabilities of the type without operating on it directly.
We can dispatch on
GEB:<SUBSTOBJ>
sinceDEFMETHOD
only works on Common Lisp Object System (CLOS) types and not generic types in CL.
Methods for closed and open types
With these pieces in play let us explore how we write a method in a way that is conducive to open and closed code.
(inpackage :geb)
(defgeneric topoly (morphism))
(defmethod topoly ((obj <substmorph>))
(typecaseof substmorph obj
(alias ...)
(substobj (error "Impossible")
(init 0)
(terminal 0)
(injectleft poly:ident)
(injectright ...)
(comp ...)
(case ...)
(pair ...)
(projectright ...)
(projectleft ...)
(distribute ...)
(otherwise (subclassresponsibility obj))))
(defmethod topoly ((obj <substobj>))
(declare (ignore obj))
poly:ident)
In this piece of code we can notice a few things:
We case on
GEB:SUBSTMORPH
exhaustivelyWe cannot hit the
GEB:<SUBSTOBJ>
case due to method dispatchWe have this
GEB.UTILS:SUBCLASSRESPONSIBILITY
function getting called.We can write further methods extending the function to other subtypes.
Thus the GEB.COMMON:TOPOLY
function is written in such a way that it
supports a closed definition and open extensions, with
GEB.UTILS:SUBCLASSRESPONSIBILITY
serving to be called if an
extension a user wrote has no handling of this method.
Code can also be naturally written in a more open way as well, by simply running methods on each class instead.
Potential Drawback and Fixes
One nasty drawback is that we can't guarantee the method exists. In java this can easily be done with interfaces and then enforcing they are fulfilled. Sadly CL has no such equivalent. However, this is all easily implementable. If this ever becomes a major problem, it is trivial to implement this by registering the subclasses, and the perspective methods, and scouring the image for instance methods, and computing if any parent class that isn't the one calling responsibility fulfills it. Thus, in practice, you should be able to ask the system if any particular extension fulfills what extension sets that the base object has and give CI errors if they are not fulfilled, thus enforcing closed behavior when warranted.
6.3 ≺Types≻
These refer to the open type variant to a closed type. Thus when
one sees a type like GEB:GEB:SUBSTOBJ
. Read Open Types versus Closed Types for information on how to use them.
7 The Geb Model
[in package GEB]
Everything here relates directly to the underlying machinery of GEB, or to abstractions that help extend it.
7.1 The Categorical Interface
[in package GEB.MIXINS]
This covers the main Categorical interface required to be used and contained in various data structures
[genericfunction] DOM CATMORPH
Grabs the domain of the morphism. Returns a
CATOBJ
[genericfunction] CODOM CATMORPH
Grabs the codomain of the morphism. Returns a
CATOBJ
[genericfunction] CURRYPROD CATMORPH CATLEFT CATRIGHT
Curries the given product type given the product. This returns a
CATMORPH
.This interface version takes the left and right product type to properly dispatch on. Instances should specalize on the
CATRIGHT
argumentUse
GEB.MAIN:CURRY
instead.
7.2 Geneircs
[in package GEB.GENERICS]
These functions represent the generic functions that can be run on many parts of the compiler, they are typically rexported on any package that implements the given generic function.
You can view their documentation in their respective API sections.
The main documentation for the functionality is given here, with examples often given in the specific methods
[genericfunction] GAPPLY MORPHISM OBJECT
Applies a given Moprhism to a given object.
This is practically a naive interpreter for any category found throughout the codebase.
Some example usages of
GAPPLY
are.GEB> (gapply (comp (mcase gebbool:true gebbool:not) (>right so1 gebbool:bool)) (left so1)) (right s1) GEB> (gapply (comp (mcase gebbool:true gebbool:not) (>right so1 gebbool:bool)) (right so1)) (left s1)
[genericfunction] WELLDEFPCAT MORPHISM
Given a moprhism of a category, checks that it is welldefined. E.g. that composition of morphism is welldefined by checking that the domain of MCAR corresponds to the codomain of MCADR
[genericfunction] MAYBE OBJECT
Wraps the given
OBJECT
into a Maybe monad The Maybe monad in this case is simply wrapping the term in a coprod of so1(0
1
)
[genericfunction] SOHOMOBJ OBJECT1 OBJECT2
Takes in X and Y Geb objects and provides an internal homobject (sohomobj X Y) representing a set of functions from X to Y
[genericfunction] SOEVAL OBJECT1 OBJECT2
Takes in X and Y Geb objects and provides an evaluation morphism (prod (sohomobj X Y) X) > Y
[genericfunction] WIDTH OBJECT
Given an
OBJECT
of Geb presents it as a SeqN object. That is, width corresponds the object part of the toseqn functor.
[genericfunction] TOCIRCUIT MORPHISM NAME
Turns a
MORPHISM
into a Vampir circuit. theNAME
is the given name of the output circuit.
[genericfunction] TOBITC MORPHISM
Turns a given
MORPHISM
into aGEB.BITC.SPEC:BITC
[genericfunction] TOSEQN MORPHISM
Turns a given
MORPHISM
into aGEB.SEQN.SPEC:SEQN
[genericfunction] TOPOLY MORPHISM
Turns a given
MORPHISM
into aGEB.POLY.SPEC:POLY
[genericfunction] TOCAT CONTEXT TERM
Turns a
MORPHISM
with a context into Geb's Core category
[genericfunction] TOVAMPIR MORPHISM VALUES CONSTRAINTS
Turns a
MORPHISM
into a Vampir circuit, with concrete values.The more natural interface is
TOCIRCUIT
, however this is a more low level interface into what the polynomial categories actually implement, and thus can be extended or changed.The
VALUES
are likely vampir values in a list.The
CONSTRAINTS
represent constraints that get creating
7.3 Core Category
[in package GEB.SPEC]
The underlying category of GEB. With Subst Obj covering the shapes and forms (GEBDOCS/DOCS:@OBJECTS) of data while Subst Morph deals with concrete GEBDOCS/DOCS:@MORPHISMS within the category.
From this category, most abstractions will be made, with
SUBSTOBJ
serving as a concrete type layout, with
SUBSTMORPH
serving as the morphisms between different
SUBSTOBJ
types. This category is equivalent to
finset.
A good example of this category at work can be found within the Booleans section.
7.3.1 Subst Obj
This section covers the objects of the SUBSTMORPH
category. Note that SUBSTOBJ
refers to the
closed type, whereas <SUBSTOBJ>
refers
to the open type that allows for user extension.
[class] <SUBSTOBJ> <SUBSTMORPH> DIRECTPOINTWISEMIXIN METAMIXIN CATOBJ
the class corresponding to
SUBSTOBJ
. See GEBDOCS/DOCS:@OPENCLOSED
SUBSTOBJ
type is not a constructor itself, instead it's
best viewed as the sum type, with the types below forming the
constructors for the term. In ML we would write it similarly to:
type substobj = so0
 so1
 prod
 coprod

The PRODUCT object. Takes two
CATOBJ
values that get put into a pair.The formal grammar of PRODUCT is
(prod mcar mcadr)
where
PROD
is the constructor,MCAR
is the left value of the product, andMCADR
is the right value of the product.Example:
(gebgui::visualize (prod gebbool:bool gebbool:bool))
Here we create a product of two
GEBBOOL:BOOL
types.

the COPRODUCT object. Takes
CATOBJ
values that get put into a choice of either value.The formal grammar of PRODUCT is
(coprod mcar mcadr)
Where CORPOD is the constructor,
MCAR
is the left choice of the sum, andMCADR
is the right choice of the sum.Example:
(gebgui::visualize (coprod so1 so1))
Here we create the boolean type, having a choice between two unit values.

The Initial Object. This is sometimes known as the VOID type.
the formal grammar of
SO0
isso0
where
SO0
isTHE
initial object.Example
lisp

The Terminal Object. This is sometimes referred to as the Unit type.
the formal grammar or
SO1
isso1
where
SO1
isTHE
terminal objectExample
(coprod so1 so1)
Here we construct
GEBBOOL:BOOL
by simply stating that we have the terminal object on either side, giving us two possible ways to fill the type.(>left so1 so1) (>right so1 so1)
where applying
>LEFT
gives us the left unit, while>RIGHT
gives us the right unit.
The Accessors specific to Subst Obj
7.3.2 Subst Morph
The overarching types that categorizes the SUBSTMORPH
category. Note that SUBSTMORPH
refers to the
closed type, whereas <SUBSTMORPH>
refers
to the open type that allows for user extension.

The morphisms of the
SUBSTMORPH
category
[class] <SUBSTMORPH> DIRECTPOINTWISEMIXIN METAMIXIN CATMORPH
the class type corresponding to
SUBSTMORPH
. See GEBDOCS/DOCS:@OPENCLOSED
SUBSTMORPH
type is not a constructor itself, instead it's
best viewed as the sum type, with the types below forming the
constructors for the term. In ML we would write it similarly to:
type substmorph = comp
 substobj
 case
 init
 terminal
 pair
 distribute
 injectleft
 injectright
 projectleft
 projectright
Note that an instance of SUBSTOBJ
, acts like the identity
morphism to the layout specified by the given SUBSTOBJ
. Thus
we can view this as automatically lifting a SUBSTOBJ
into a
SUBSTMORPH

The composition morphism. Takes two
CATMORPH
values that get applied in standard composition order.The formal grammar of
COMP
is(comp mcar mcadr)
which may be more familiar as
g 。f
Where
COMP
( 。) is the constructor,MCAR
(g) is the second morphism that gets applied, andMCADR
(f) is the first morphism that gets applied.Example:
(gebgui::visualize (comp (<right so1 gebbool:bool) (pair (<left so1 gebbool:bool) (<right so1 gebbool:bool))))
In this example we are composing two morphisms. the first morphism that gets applied (
PAIR
...) is the identity function on the type (PROD
SO1
GEBBOOL:BOOL
), where we pair the left projection and the right projection, followed by taking the right projection of the type.Since we know (
COMP
f id) is just f per the laws of category theory, this expression just reduces to(<right so1 gebbool:bool)

Eliminates coproducts. Namely Takes two
CATMORPH
values, one gets applied on the left coproduct while the other gets applied on the right coproduct. The result of eachCATMORPH
values must be the same.The formal grammar of
CASE
is:(mcase mcar mcadr)
Where
MCASE
is the constructor,MCAR
is the morphism that gets applied to the left coproduct, andMCADR
is the morphism that gets applied to the right coproduct.Example:
(comp (mcase gebbool:true gebbool:not) (>right so1 gebbool:bool))
In the second example, we inject a term with the shape
GEBBOOL:BOOL
into a pair with the shape (SO1
×GEBBOOL:BOOL
), then we useMCASE
to denote a morphism saying.IF
the input is of the shapeSO1
(0
1
), then give us True, otherwise flip the value of the boolean coming in.

The INITIAL Morphism, takes any
CATOBJ
and creates a moprhism fromSO0
(also known as void) to the object given.The formal grammar of INITIAL is
(init obj)
where
INIT
is the constructor.OBJ
is the type of object that will be conjured up fromSO0
, when the morphism is applied onto an object.Example:
(init so1)
In this example we are creating a unit value out of void.

The
TERMINAL
morphism, Takes anyCATOBJ
and creates a morphism from that object toSO1
(also known as unit).The formal grammar of
TERMINAL
is(terminal obj)
where
TERMINAL
is the constructor.OBJ
is the type of object that will be mapped toSO1
, when the morphism is applied onto an object.Example:
(terminal (coprod so1 so1)) (gebgui::visualize (terminal (coprod so1 so1))) (comp value (terminal (codomain value))) (comp true (terminal bool))
In the first example, we make a morphism from the corpoduct of
SO1
andSO1
(essentiallyGEBBOOL:BOOL
) toSO1
.In the third example we can proclaim a constant function by ignoring the input value and returning a morphism from unit to the desired type.
The fourth example is taking a
GEBBOOL:BOOL
and returningGEBBOOL:TRUE
.

Introduces products. Namely Takes two
CATMORPH
values. When thePAIR
morphism is applied on data, these twoCATMORPH
's are applied to the object, returning a pair of the resultsThe formal grammar of constructing an instance of pair is:
(pair mcar mcdr)
where
PAIR
is the constructor,MCAR
is the left morphism, andMCDR
is the right morphismExample:
(pair (<left so1 gebbool:bool) (<right so1 gebbool:bool)) (gebgui::visualize (pair (<left so1 gebbool:bool) (<right so1 gebbool:bool)))
Here this pair morphism takes the pair
SO1
(0
1
) ×GEBBOOL:BOOL
, and projects back the left fieldSO1
as the first value of the pair and projects back theGEBBOOL:BOOL
field as the second values.
[class] DISTRIBUTE <SUBSTMORPH>
The distributive law
[class] INJECTLEFT <SUBSTMORPH>
The left injection morphism. Takes two
CATOBJ
values. It is the dual ofINJECTRIGHT
The formal grammar is
(>left mcar mcadr)
Where
>LEFT
is the constructor,MCAR
is the value being injected into the coproduct ofMCAR
+MCADR
, and theMCADR
is just the type for the unused right constructor.Example:
(gebgui::visualize (>left so1 gebbool:bool)) (comp (mcase gebbool:true gebbool:not) (>left so1 gebbool:bool))
In the second example, we inject a term with the shape
SO1
(0
1
) into a pair with the shape (SO1
×GEBBOOL:BOOL
), then we useMCASE
to denote a morphism saying.IF
the input is of the shapeSO1
(0
1
), then give us True, otherwise flip the value of the boolean coming in.
[class] INJECTRIGHT <SUBSTMORPH>
The right injection morphism. Takes two
CATOBJ
values. It is the dual ofINJECTLEFT
The formal grammar is
(>right mcar mcadr)
Where
>RIGHT
is the constructor,MCADR
is the value being injected into the coproduct ofMCAR
+MCADR
, and theMCAR
is just the type for the unused left constructor.Example:
(gebgui::visualize (>right so1 gebbool:bool)) (comp (mcase gebbool:true gebbool:not) (>right so1 gebbool:bool))
In the second example, we inject a term with the shape
GEBBOOL:BOOL
into a pair with the shape (SO1
×GEBBOOL:BOOL
), then we useMCASE
to denote a morphism saying.IF
the input is of the shapeSO1
(0
1
), then give us True, otherwise flip the value of the boolean coming in.
[class] PROJECTLEFT <SUBSTMORPH>
The
LEFT
PROJECTION. Takes twoCATMORPH
values. When theLEFT
PROJECTION morphism is then applied, it grabs the left value of a product, with the type of the product being determined by the twoCATMORPH
values given.the formal grammar of a
PROJECTLEFT
is:(<left mcar mcadr)
Where
<LEFT
is the constructor,MCAR
is the left type of the PRODUCT andMCADR
is the right type of the PRODUCT.Example:
(gebgui::visualize (<left gebbool:bool (prod so1 gebbool:bool)))
In this example, we are getting the left
GEBBOOL:BOOL
from a product with the shape
[class] PROJECTRIGHT <SUBSTMORPH>
The
RIGHT
PROJECTION. Takes twoCATMORPH
values. When theRIGHT
PROJECTION morphism is then applied, it grabs the right value of a product, with the type of the product being determined by the twoCATMORPH
values given.the formal grammar of a
PROJECTRIGHT
is:(<right mcar mcadr)
Where
<RIGHT
is the constructor,MCAR
is the right type of the PRODUCT andMCADR
is the right type of the PRODUCT.Example:
(gebgui::visualize (comp (<right so1 gebbool:bool) (<right gebbool:bool (prod so1 gebbool:bool))))
In this example, we are getting the right
GEBBOOL:BOOL
from a product with the shape
The Accessors specific to Subst Morph
7.3.3 Realized Subst Objs
This section covers the REALIZEDOBJECT
type. This
represents a realized SUBSTOBJ
term.
The REALIZEDOBJECT
is not a real constructor but rather a sum
type for the following type
(deftype realizedobject () `(or left right list so1 so0))
In ML we would have written something like
type realizedobject = so0
 so1
 list
 left
 right

A realized object that can be sent into.
Lists represent
PROD
in the<SUBSTOBJ>
category
 [function] LEFT OBJ
 [function] RIGHT OBJ
7.4 Accessors
[in package GEB.UTILS]
These functions are generic lenses of the GEB codebase. If a class is defined, where the names are not known, then these accessors are likely to be used. They may even augment existing classes.

Grabs the underlying object

the name of the given object

the function of the object
[genericfunction] PREDICATE OBJ
the
PREDICATE
of the object

the then branch of the object

the then branch of the object

the code of the object
7.5 Constructors
[in package GEB.SPEC]
The API for creating GEB terms. All the functions and variables here relate to instantiating a term
[variable] *SO0* s0
The Initial Object
[variable] *SO1* s1
The Terminal Object
More Ergonomic API variants for *SO0*
and *SO1*
 [function] MAKEALIAS &KEY NAME OBJ
 [function] HASALIASP OBJ
[function] <LEFT MCAR MCADR
projects left constructor
[function] <RIGHT MCAR MCADR
projects right constructor
[function] >LEFT MCAR MCADR
injects left constructor
[function] >RIGHT MCAR MCADR
injects right constructor
 [function] MCASE MCAR MCADR
 [function] MAKEFUNCTOR &KEY OBJ FUNC
7.6 API
Various forms and structures built ontop of Core Category
[method] GAPPLY (MORPH <SUBSTMORPH>) OBJECT
My main documentation can be found on
GAPPLY
I am the
GAPPLY
for, the OBJECT that I expect is of type REALIZEDOBJECT
. See the documentation forREALIZEDOBJECT
for the forms it can take.Some examples of me are
GEB> (gapply (comp (mcase gebbool:true gebbool:not) (>right so1 gebbool:bool)) (left so1)) (right s1) GEB> (gapply (comp (mcase gebbool:true gebbool:not) (>right so1 gebbool:bool)) (right so1)) (left s1) GEB> (gapply gebbool:and (list (right so1) (right so1))) (right s1) GEB> (gapply gebbool:and (list (left so1) (right so1))) (left s1) GEB> (gapply gebbool:and (list (right so1) (left so1))) (left s1) GEB> (gapply gebbool:and (list (left so1) (left so1))) (left s1)
[method] GAPPLY (MORPH OPAQUEMORPH) OBJECT
My main documentation can be found on
GAPPLY
I am the
GAPPLY
for a generic OPAQUEMOPRH I simply dispatchGAPPLY
on my interior codelisp GEB> (gapply (comp geblist:*car* geblist:*cons*) (list (right gebbool:trueobj) (left geblist:*nil*))) (right GEBBOOL:TRUE)
[method] GAPPLY (MORPH OPAQUE) OBJECT
My main documentation can be found on
GAPPLY
I am the
GAPPLY
for a genericOPAQUE
I simply dispatchGAPPLY
on my interior code, which is likely just an object
 [method] WELLDEFPCAT (MORPH <SUBSTMORPH>)
 [method] WELLDEFPCAT (MORPH <NATMORPH>)
 [method] WELLDEFPCAT (MORPH <NATOBJ>)
7.6.1 Booleans
[in package GEBBOOL]
Here we define out the idea of a boolean. It comes naturally from the concept of coproducts. In ML they often define a boolean like
data Bool = False  True
We likewise define it with coproducts
(def bool (coprod so1 so1))
(def true (>right so1 so1))
(def false (>left so1 so1))
The functions given work on this.

The true value of a boolean type. In this case we've defined true as the right unit

The false value of a boolean type. In this case we've defined true as the left unit

The Boolean Type, composed of a coproduct of two unit objects
(coprod so1 so1)
7.6.2 Lists
[in package GEBLIST]
Here we define out the idea of a List. It comes naturally from the
concept of coproducts. Since we lack polymorphism this list is
concrete over GEBBOOL:@GEBBOOL
In ML syntax it looks like
data List = Nil  Cons Bool List
We likewise define it with coproducts, with the recursive type being opaque
(defparameter *nil* (so1))
(defparameter *constype* (reference 'cons))
(defparameter *canonicalconstype*
(opaque 'cons
(prod gebbool:bool *constype*)))
(defparameter *list*
(coprod *nil* *constype*))
The functions given work on this.
 [variable] *NIL* NIL
 [variable] *CONSTYPE* CONS
 [variable] *LIST* LIST
 [variable] *CAR* CAR
 [variable] *CONS* CONSΜ
 [variable] *CDR* CDR
7.6.3 Translation Functions
[in package GEB.TRANS]
These cover various conversions from Subst Morph and Subst Obj into other categorical data structures.
[method] TOCIRCUIT (OBJ <SUBSTMORPH>) NAME
Turns a Subst Morph to a VampIR Term

Produces a list of zeroes Currently not aligning with semantics of dropwidth as domain and codomain can be of differing lengths
[method] TOSEQN (OBJ INJECTLEFT)
Injects an x by marking its entries with 0 and then inserting as padded bits if necessary
[method] TOSEQN (OBJ INJECTRIGHT)
Injects an x by marking its entries with 1 and then inserting as padded bits if necessary

Cases by forgetting the padding and if necessary dropping the extra entries if one of the inputs had more of them to start with
[method] TOSEQN (OBJ DISTRIBUTE)
Given A x (B + C) simply moves the 1bit entry to the front and keep the same padding relations to get ((A x B) + (A x C)) as times appends sequences
7.6.4 Utility
[in package GEB.MAIN]
Various utility functions ontop of Core Category
[function] PAIRTOLIST PAIR &OPTIONAL ACC
converts excess pairs to a list format
[function] SAMETYPETOLIST PAIR TYPE &OPTIONAL ACC
converts the given type to a list format
[function] CLEAVE V1 &REST VALUES
Applies each morphism to the object in turn.
[function] CONST F X
The constant morphism.
Takes a morphism from
SO1
to a desired value of type $B$, along with a<SUBSTOBJ>
that represents the input type say of type $A$, giving us a morphism from $A$ to $B$.Thus if:
F
:SO1
→ a,X
: bthen: (const f x) : a → b
Γ, f : so1 → b, x : a  (const f x) : a → b
Further, If the input
F
has anALIAS
, then we wrap the output in a new alias to denote it's a constant version of that value.Example:
(const true bool) ; bool > bool
 [function] COMMUTES X Y
[function] COMMUTESLEFT MORPH
swap the input domain of the given catmorph
In order to swap the domain we expect the catmorph to be a
PROD
Thus if:
(dom morph) ≡ (prod x y)
, for anyx
,y
CATOBJ
then:
(commutesleft (dom morph)) ≡ (prod y x)
uΓ, f : x × y → a  (commutesleft f) : y × x → a
 [function] !> A B
 [method] SOHOMOBJ (X <NATOBJ>) Z
 [method] SOHOMOBJ (X <SUBSTOBJ>) Z
[genericfunction] SOCARDALG OBJ
Gets the cardinality of the given object, returns a
FIXNUM
 [method] SOCARDALG (OBJ <SUBSTOBJ>)

Curries the given object, returns a catmorph
The catmorph given must have its
DOM
be of aPROD
type, asCURRY
invokes the idea ofif f : (
PROD
a b) → cfor all
a
,b
, andc
being an element of catmorphthen: (curry f): a → c^b
where c^b means c to the exponent of b (
EXPT
c b)Γ, f : a × b → c,  (curry f) : a → c^b
In category terms,
a → c^b
is isomorphic toa → b → c
[function] COPRODMOR F G
Given f : A → B and g : C → D gives appropriate morphism between
COPROD
objects f x g : A + B → C + D via the unversal property. That is, the morphism part of the coproduct functor Geb x Geb → Geb
[function] PRODMOR F G
Given f : A → B and g : C → D gives appropriate morphism between
PROD
objects f x g : A x B → C x D via the unversal property. This is the morphism part of the product functor Geb x Geb → Geb
[function] UNCURRY Y Z F
Given a morphism f : x → z^y and explicitly given y and z variables produces an uncurried version f' : x × y → z of said morphism
[genericfunction] TEXTNAME MORPH
Gets the name of the moprhism
These utilities are ontop of CATOBJ
[method] MAYBE (OBJ <SUBSTOBJ>)
I recursively add maybe terms to all
terms, for what maybe means checkout my generic function documentation. turning products of A x B into Maybe (Maybe A x Maybe B),
turning coproducts of A  B into Maybe (Maybe A  Maybe B),
7.7 Examples
PLACEHOLDER: TO SHOW OTHERS HOW EXAMPLE
s WORK
Let's see the transcript of a real session of someone working with GEB:
(values (princ :hello) (list 1 2))
.. HELLO
=> :HELLO
=> (1 2)
(+ 1 2 3 4)
=> 10
8 Extension Sets for Categories
[in package GEB.EXTENSION.SPEC]
This package contains many extensions one may see over the codebase.
Each extension adds an unique feature to the categories they are extending. To learn more, read about the individual extension you are interested in.
Common Sub expressions represent repeat logic that can be found throughout any piece of code
[class] COMMONSUBEXPRESSION DIRECTPOINTWISEMIXIN METAMIXIN CATMORPH
I represent common subexpressions found throughout the code.
I implement a few categorical extensions. I am a valid
CATMORPH
along with fulling the interface for the GEB.POLY.SPEC:( 0
1
) category.The name should come from an algorithm that automatically fines common subexpressions and places the appropriate names.
 [function] MAKECOMMONSUBEXPRESSION &KEY OBJ NAME
The Opaque extension lets users write categorical objects and morphisms where their implementation hide the specifics of what types they are operating over
[class] OPAQUE CATOBJ METAMIXIN
I represent an object where we want to hide the implementation details of what kind of
GEB:SUBSTOBJ
I am.
[class] REFERENCE CATOBJ CATMORPH DIRECTPOINTWISEMIXIN METAMIXIN
I represent a reference to an
OPAQUE
identifier.
[class] OPAQUEMORPH CATMORPH METAMIXIN
This represents a morphsim where we want to deal with an
OPAQUE
that we know intimate details of
 [function] REFERENCE NAME
 [function] OPAQUEMORPH CODE &KEY (DOM (
DOM
CODE
)) (CODOM (CODOM
CODE
))
 [function] OPAQUE NAME CODE
The Natural Object/Morphism extension allows to expand the core Geb category with additional constructors standing in for btsequence representation of natural numbers along with basic operation relating to those.
[class] <NATOBJ> DIRECTPOINTWISEMIXIN METAMIXIN CATOBJ CATMORPH
the class corresponding to
NATOBJ
, the extension of SUBSTOBJ adding to Geb bit representation of natural numbers.

the
NATWIDTH
object. Takes a nonzero natural numberNUM
and produces an object standing for cardinality 2^(NUM
) corresponding toNUM
wide bit number.The formal grammar of
NATWIDTH
is(natwidth num)
where
NATWIDTH
is the constructor,NUM
the choice of a natural number we want to be the width of the bits we are to consder.
 [function] NATWIDTH NUM
[class] <NATMORPH> DIRECTPOINTWISEMIXIN METAMIXIN CATMORPH
the class corresponding to
NATMORPH
, the extension of SUBSTMORPH adding to Geb basic operations on bit representations of natural numbers

Given a natural number
NUM
greater than 0, gives a morphsm (natadd num) : (natmod num) x (natmod num) > (natmod num) representing floored addition of two bits of length n.The formal grammar of
NATADD
islisp (natadd num)

Given a natural number
NUM
greater than 0, gives a morphsm (natmult num) : (natmod num) x (natmod num) > (natmod n) representing floored multiplication in natural numbers modulo n.The formal grammar of
NATMULT
islisp (natmult num)

Given a natural number
NUM
greater than 0, gives a morphsm (natsub sum) : (natmod num) x (natmod num) > (natmod num) representing floored subtraction of two bits of length n.The formal grammar of
NATSUB
islisp (natsub num)

Given a natural number
NUM
greater than 0, gives a morphsm (natdiv num) : (natmod num) x (natmod num) > (natmod num) representing floored division in natural numbers modulo n.The formal grammar of
NATDIV
islisp (natdiv num)

Given a
NUM
natural number, gives a morphsm (natconst num pos) : so1 > (natwidth num).That is, chooses the
POS
natural number as aNUM
wide bit numberThe formal grammar of
NATADD
islisp (natconst num pos)

Given a nutural number
NUM
presents aNUM
wide bit number as a (NUM
+ 1)wide bit number via injecting.The formal grammar of
NATINJ
is(natinj num)
In Geb, the injection presents itself as a morphism (natwidth num) > (natwidth (1 + num))

Given two natural numbers of bit length n and m, concatenates them in that order giving a bit of length n + m.
The formal grammar of
NATCONCAT
is(natconcat numleft numright)
In Geb this corresponds to a morphism (natwidth numleft) x (natwidth numright) > (natwidth (n + m))
For a translation to SeqN simply take x of n width and y of m with and take x^m + y
[class] ONEBITTOBOOL <NATMORPH>
A map natwidth 1 > bool sending #0 to false and #1 to true
[class] NATDECOMPOSE <NATMORPH>
Morphism natwidth n > (natwidth 1) x (natwidth (1 n)) splitting a natural number into the last and all but last collection of bits

Morphism natwidth n x natwidth n > bool which evaluated to true iff both inputs are the same

Morphism natwidth n x natwidth n > bool which evaluated to true iff the first input is less than the second

Morphism natwidth n x natwidth n > natwidth n which takes a modulo of the left projection of a pair by the second projection of a pari
 [function] NATADD NUM
 [function] NATMULT NUM
 [function] NATSUB NUM
 [function] NATDIV NUM
 [function] NATCONST NUM POS
 [function] NATINJ NUM
 [function] NATCONCAT NUMLEFT NUMRIGHT
 [function] NATEQ NUM
 [function] NATLT NUM
 [function] NATMOD NUM
 [variable] *ONEBITTOBOOL* #<ONEBITTOBOOL {1006996C63}>
9 The GEB GUI
[in package GEBGUI]
This section covers the suite of tools that help visualize geb objects and make the system nice to work with
9.1 Visualizer
The GEB visualizer deals with visualizing any objects found in the Core Category
if the visualizer gets a Subst Morph, then it will show how
the GEB:SUBSTMORPH
changes any incoming term.
if the visualizer gets a Subst Obj, then it shows the data layout of the term, showing what kind of data
[function] VISUALIZE OBJECT &OPTIONAL (ASYNC
T
)Visualizes both Subst Obj and Subst Morph objects

Kills all threads and open gui objects created by
VISUALIZE
9.1.1 Aiding the Visualizer
One can aid the visualization process a bit, this can be done by
simply placing ALIAS
around the object, this will place it
in a box with a name to better identify it in the graphing procedure.
9.2 Export Visualizer
This works like the normal visualizer except it exports it to a file to be used by other projects or perhaps in papers
[function] SVG OBJECT PATH &KEY (DEFAULTVIEW (
MAKEINSTANCE
'SHOWVIEW
))Runs the visualizer, outputting a static
SVG
image at the directory of choice.You can customize the view. By default it uses the showview, which is the default of the visualizer.
A good example usage is
GEBTEST> (gebgui:svg (shallowcopyobject gebbool:and) "/tmp/foo.svg")
9.3 The GEB Graphizer
[in package GEBGUI.GRAPHING]
This section covers the GEB Graph representation
9.3.1 The GEB Graphizer Core
[in package GEBGUI.CORE]
This section covers the graphing procedure in order to turn a GEB object into a format for a graphing backend.
The core types that facilittate the functionality

A note is a note about a new node in the graph or a note about a
NODE
which should be merged into an upcomingNODE
.An example of a
NODENOTE
would be in the case of pair(pair g f)
Π₁ f> Y X > [Y × Z] g> Z Π₂
An example of a MERGENOTE
(Case f g) (COMP g f)
χ₁ > X f [X + Y] > A > Y g/ χ₂ X f> Y > Y g> Z
Notice that in the pair case, we have a note and a shared node to place down, where as in both of the MERGENOTE examples, the Note at the end is not prepended by any special information

I represent a graphical node structure. I contain my children and a value to display, along with the representation for which the node really stands for.
Further, we derive the metamixin, as it's important for arrow drawing to know if we are the left or the right or the nth child of a particular node. This information is tracked, by storing the object that goes to it in the meta table and recovering the note.

This note should be squashed into another note and or node.
 [function] MAKENOTE &REST INITARGS &KEY FROM NOTE VALUE &ALLOWOTHERKEYS
 [function] MAKESQUASH &REST INITARGS &KEY VALUE &ALLOWOTHERKEYS
[genericfunction] GRAPHIZE MORPH NOTES
Turns a morphism into a node graph.
The
NOTES
serve as a way of sharing and continuing computation.If the
NOTE
is a:SHARED
NOTE
then it represents aNODE
without children, along with saying where it came from. This is to be stored in parent of theNOTE
If the
NOTE
is a:CONTINUE
NOTE
, then the computation is continued at the spot.The parent field is to set the note on the parent if the
NOTE
is going to be merged
 [genericfunction] VALUE OBJECT
[function] CONSNOTE NOTE NOTES
Adds a note to the notes list.
[function] APPLYNOTE NOTETOBEON NOTE
Here we apply the
NOTE
to theNODE
.In the case of a new node, we record down the information in the note, and set the note as the child of the current
NODE
. TheNODE
is returned.In the case of a squashnote, we instead just return the squashnote as that is the proper
NODE
to continue from
 [genericfunction] REPRESENTATION OBJECT
 [genericfunction] CHILDREN OBJECT
[function] DETERMINETEXTANDOBJECTFROMNODE FROM TO
Helps lookup the text from the node
[function] NOTERIZECHILDREN NODE FUNC
Applies a specified note to the
CHILDREN
of theNODE
.It does this by applying
FUNC
on all theCHILDREN
and the index of the child in the list
[function] NOTORIZECHILDRENWITHINDEXSCHEMA PREFIX NODE
Notorizes the node with a prefix appended with the subscripted number
9.3.2 The GEB Graphizer Passes
[in package GEBGUI.GRAPHING.PASSES]
This changes how the graph is visualized, simplifying the graph in ways that are intuitive to the user
[function] PASSES NODE
Runs all the passes that simplify viewing the graph. These simplifications should not change the semantics of the graph, only display it in a more bearable way
10 Seqn Specification
[in package GEB.SEQN]
This covers a GEB view of multibit sequences. In particular this type will be used in translating GEB's view of multibit sequences into Vampir
10.1 Seqn Types
[in package GEB.SEQN.SPEC]
[class] <SEQN> DIRECTPOINTWISEMIXIN CATMORPH
Seqn is a category whose objects are finite sequences of natural numbers. The nth natural number in the sequence represents the bitwidth of the nth entry of the corresponding polynomial circuit
Entries are to be read as (x_1,..., x_n) and x_i is the ith entry So car of a such a list will be the first entry, this is the dissimilarity with the bit notation where newer entries come first in the list
We interpret pairs as actual pairs if entry is of width above 0 and drop it otherwise in the VampIr setup so that ident bool x bool goes to name x1 = x1 as (seqwidth bool) = (1, max(0, 0))

composes the
MCAR
andMCADR
morphisms f : (a1,...,an) > (b1,..., bm), g : (b1,...,bm) > (c1, ..., ck) compose g f : (a1,...,an) > (c1,...,cn)

For f : (a1,..., an) > (x1,...,xk), g : (b1,..., bm) > (y1,...,yl) parallel f g : (a1,...,an, b1,...bm) > (x1,...,xk,y1,...,yl)

Copies the
MCAR
of length n onto length 2*n by copying its inputs (MCAR
). fork (a1, ...., an) > (a1,...,an, a1,..., an)

Drops everything onto a 0 vector, the terminal object dropnil (x1, ..., xn) : (x1,...,xn) > (0)

Removes an extra 0 entry from
MCAR
on the right remove (x1,...,xn) : (x1,...,xn, 0) > (x1,...,xn)

Removes an extra 0 entry from
MCAR
on the left remove (x1,...,xn) : (0, x1,...,xn) > (x1,...,xn)

Given two vectors of same length but with the first ones of padded width, simply project the core bits without worrying about extra zeroes at the end if they are not doing any work dropwidth (x1,...,xn) (y1,...,yn) : (x1,...,xn) > (y1,...,yn) where xi > yi for each i and entries need to be in the image of the evident injection map
In other words the constraints here are that on the enput ei corresponding to xi bit entry the constraint is that range yi ei is true alongside the usual (isrange xi ei) constraint
Another implementation goes through manual removal of extra bits (specifically xiyi bits) to the left after the decomposition by range xi
[class] INJLENGTHLEFT <SEQN>
Taken an
MCAR
vector appends to itMCADR
list of vectors with arbitrary bit length by doing nothing on the extra entries, i.e. just putting 0es there. injlenghleft (x1,...,xn) (y1,...,ym): (x1,...,xn) > (x1,...,xn, y1,...,yn) Where 0es go in the place of ys or nothing if the injection is into 0bitsSo what gets injected is the left part
[class] INJLENGTHRIGHT <SEQN>
Taken an
MCADR
vector appends to itMCAR
list of vectors with arbitrary bit length by doing nothing on the extra entries, i.e. just putting 0es there. injlenghright (x1,...,xn) (y1,...,ym): (y1,...,ym) > (x1,...,xn, y1,...,yn) Where 0es go in the place of xs. If any of yi's are 0bit vectors, the injection goes to nil entry on those partsWhat gets injected is the right part

Taken an
MCAR
1long and injects it toMCADR
wide slot wider than the original one by padding it with 0es on the left. injsize x1 m: (x1) > (m)Just a special case of dropwidth

Takes an f: (x1,...,xn) > c, g : (x1,...,xn) >c and produces branchseq f g (1, x1,...,xn) > c acting as f on 0 entry and g on 1

Takes an
MCAR
sequence of length at leastMCADR
and shifts theMCADR
entry to the front shiftfront (x1,...,xn) k : (x1,...,xk,...,xn) > (xk, x1,..., x_k1, x_k+1,...,xn)

Compiles to rangechecked addition of natural numbers of
MCAR
width. seqnadd n : (n, n) > (n)

Compiles to negativechecked subtraction of natural numbers of
MCAR
width. seqnsubtract n : (n, n) > (n)

Compiles to rangechecked multiplication of natural numbers of
MCAR
width. seqnmultiply n : (n, n) > (n)

Compiles to usual VampIR floored multiplication of natural numbers of
MCAR
width. seqndivide n : (n, n) > (n)

Takes a number of
MCAR
andMCADR
width and produces a number ofMCAR
+MCADR
width by concatenating the bit representations. Using field elements, this translates to multiplying the first input by 2 to the power ofMCADR
and summing with the second entry seqnconcat n m = (n, m) > (n+m)

The type signature of the morphism is seqndocompose n : (n) > (1, (n  1)) with the intended semantics being that the morphism takes an nbit integer and splits it, taking the leftmost bit to the left part of the codomain and the rest of the bits to the righ

The type signature of the morphism is seqneq n : (n, n) > (1, 0) with the intended semantics being that the morphism takes two nbit integers and produces 1 iff they are equal

The type signature of the morphism is seqneq n : (n, n) > (1, 0) with the intended semantics being that the morphism takes two nbit integers and produces 1 iff the first one is less than the second

The type signature of the morphism is seqnmod n : (n, n) > (n) with the intended semantics being that the morphism takes two nbit integers and produces the modulo of the first integer by the second
10.2 Seqn Constructors
[in package GEB.SEQN.SPEC]
Every accessor for each of the classes making up seqn
 [function] COMPOSITION MCAR MCADR
 [function] ID MCAR
 [function] FORKSEQ MCAR
 [function] PARALLELSEQ MCAR MCADR
 [function] DROPNIL MCAR
 [function] REMOVERIGHT MCAR
 [function] REMOVELEFT MCAR
 [function] DROPWIDTH MCAR MCADR
 [function] INJLENGTHLEFT MCAR MCADR
 [function] INJLENGTHRIGHT MCAR MCADR
 [function] INJSIZE MCAR MCADR
 [function] BRANCHSEQ MCAR MCADR
 [function] SHIFTFRONT MCAR MCADR
 [function] SEQNADD MCAR
 [function] SEQNSUBTRACT MCAR
 [function] SEQNMULTIPLY MCAR
 [function] SEQNDIVIDE MCAR
 [function] SEQNNAT MCAR MCADR
 [function] SEQNCONCAT MCAR MCADR
 [function] SEQNDECOMPOSE MCAR
 [function] SEQNEQ MCAR
 [function] SEQNLT MCAR
 [function] SEQNMOD MCAR
10.3 seqn api
[in package GEB.SEQN.MAIN]
this covers the seqn api
[function] FILLIN NUM SEQ
Fills in extra inputs on the right with 0oes
[function] PRODLIST L1 L2
Takes two lists of same length and gives pointwise product where first element come from first list and second from second
SEQN> (prodlist (list 1 2) (list 3 4)) ((1 3) (2 4))
[function] SEQMAXFILL SEQ1 SEQ2
Takes two lists, makes them same length by adding 0es on the right where necessary and takes their pointwise product
[function] INJCOPRODPARALLEL OBJ COPR
takes an width(A) or width(B) already transformed with a width(A+B) and gives an appropriate injection of (a1,...,an) into (max (a1, b1), ...., max(an, bn),...) i.e. where the maxes are being taken during the width operation without filling in of the smaller object
 [function] ZEROLIST LENGTH

Gives the domain of a morphism in SeqN. For a less formal desription consult the specs file

Gives the codomain of a morphism in SeqN. For a less formal description consult the specs file
 [method] WELLDEFPCAT (MORPH <SEQN>)
[method] GAPPLY (MORPHISM <SEQN>) VECTOR
Takes a list of vectors of natural numbers and gives out their evaluations. Currently does not correspond directly to the intended semantics but is capable of succesfully evaluating all compiled terms
10.4 Seqn Transformations
[in package GEB.SEQN.TRANS]
This covers transformation functions from
[method] TOCIRCUIT (MORPHISM <SEQN>) NAME
Turns a SeqN term into a VampIR Gate with the given name Note that what is happening is that we look at the domain of the morphism and skip 0es, making nonzero entries into wires
[method] TOVAMPIR (OBJ COMPOSITION) INPUTS CONSTRAINTS
Compile the
MCADR
after feeding in appropriate inputs and then feed them as entries to compiledMCAR
[method] TOVAMPIR (OBJ DROPWIDTH) INPUTS CONSTRAINTS
The compilation does not produce dropping with domain inputs wider than codomain ones appropriately. Hence we do not require range checks here and simply project
[method] TOVAMPIR (OBJ INJLENGTHLEFT) INPUTS CONSTRAINTS
Look at the
MCAR
. Look at nonnull wide entries and place 0es in the outputs otherwise ignore
[method] TOVAMPIR (OBJ INJLENGTHRIGHT) INPUTS CONSTRAINTS
Look at the
MCADR
. Look at nonnull wide entries and place 0es in the outputs
[method] TOVAMPIR (OBJ INJSIZE) INPUTS CONSTRAINTS
During th ecompilation procedure the domain will not have larger width than the codomain so we simply project
[method] TOVAMPIR (OBJ BRANCHSEQ) INPUTS CONSTRAINTS
With the leftmost input being 1 or 0, pointwise do usual bit branching. If 0 run the
MCAR
, if 1 run theMCADR
[method] TOVAMPIR (OBJ SHIFTFRONT) INPUTS CONSTRAINTS
Takes the
MCADR
entry and moves it upward leaving everything else fixed. Note that we have to be careful as inputs will have 0es removed already and hence we cannot count as usual
11 Bits (Boolean Circuit) Specification
[in package GEB.BITC]
This covers a GEB view of Boolean Circuits. In particular this type will be used in translating GEB's view of Boolean Circuits into Vampir
11.1 Bits Types
[in package GEB.BITC.SPEC]
This section covers the types of things one can find in the BIT
s(0
1
)
constructors

(parallel x y)
constructs a
PARALLEL
term where theMCAR
isx
and theMCADR
isy
,where if
x : a → b, y : c → d  (parallel x y) : a + c → b + d
then the
PARALLEL
will return a function from a and c to b and d where theMCAR
andMCADR
run on subvectors of the input.

(swap n m)
binds the
MCAR
to n andMCADR
to m, where if the input vector is of lengthn + m
, then it swaps the bits, algebraically we view it as(swap n m) : #*b₁...bₙbₙ₊₁...bₙ₊ₘ → #*bₙ₊₁...bₘ₊ₙb₁...bₙ

(branch x y)
constructs a
BRANCH
term where theMCAR
isx
and theMCADR
isy
,where if
x : a → b, y : a → b  (branch x y) : 1+a → b
then the
BRANCH
will return a function on the type1 + a
, where the 1 represents a bit to branch on. If the first bit is0
, then theMCAR
is ran, however if the bit is1
, then theMCADR
is ran.
11.2 Bits (Boolean Circuit) Constructors
[in package GEB.BITC.SPEC]
Every accessor for each of the CLASS
's found here are from Accessors
[function] COMPOSE MCAR MCADR &REST ARGS
Creates a multiway constructor for
COMPOSE
[function] FORK MCAR
FORK
ARG1
[function] PARALLEL MCAR MCADR &REST ARGS
Creates a multiway constructor for
PARALLEL
[function] SWAP MCAR MCADR
swap ARG1 and ARG2
[function] IDENT MCAR
ident ARG1
[function] DROP MCAR
drop ARG1
[function] BRANCH MCAR MCADR
branch with ARG1 or ARG2
11.3 Bits (Boolean Circuit) API
[in package GEB.BITC.MAIN]
This covers the Bits (Boolean Circuit) API
[method] GAPPLY (MORPHISM <BITC>) (OBJECT BITVECTOR)
My My main documentation can be found on
GAPPLY
I am the
GAPPLY
for<BITC>
, theOBJECT
that I expect is of typeNUMBER
.GAPPLY
reduces down to ordinary common lisp expressions rather straight forwardly;; figure out the number of bits the function takes GEBTEST> (dom (tobitc gebbool:and)) 2 (2 bits, #x2, #o2, #b10) GEBTEST> (gapply (tobitc gebbool:and) #*11) #*1 GEBTEST> (gapply (tobitc gebbool:and) #*10) #*0 GEBTEST> (gapply (tobitc gebbool:and) #*01) #*0 GEBTEST> (gapply (tobitc gebbool:and) #*00) #*0
[method] GAPPLY (MORPHISM <BITC>) (OBJECT LIST)
I am a helper gapply function, where the second argument for
<BITC>
is a list. See the docs for theBITVECTOR
version for the proper one. We do allow sending in a list like so;; figure out the number of bits the function takes GEBTEST> (dom (tobitc gebbool:and)) 2 (2 bits, #x2, #o2, #b10) GEBTEST> (gapply (tobitc gebbool:and) (list 1 1)) #*1 GEBTEST> (gapply (tobitc gebbool:and) (list 1 0)) #*0 GEBTEST> (gapply (tobitc gebbool:and) (list 0 1)) #*0 GEBTEST> (gapply (tobitc gebbool:and) (list 0 0)) #*0
11.4 Bits (Boolean Circuit) Transformations
[in package GEB.BITC.TRANS]
This covers transformation functions from
[method] TOCIRCUIT (MORPHISM <BITC>) NAME
Turns a
BITC
term into a VampIR Gate with the given name
[method] TOVAMPIR (OBJ PARALLEL) VALUES CONSTRAINTS
Take n + m bits, execute car the n bits and cadr on the m bits and concat the results from car and cadr
[method] TOVAMPIR (OBJ BRANCH) VALUES CONSTRAINTS
Look at the first bit.
If its 0, run f on the remaining bits.
If its 1, run g on the remaining bits.
12 Polynomial Specification
[in package GEB.POLY]
This covers a GEB view of Polynomials. In particular this type will be used in translating GEB's view of Polynomials into Vampir
12.1 Polynomial Types
[in package GEB.POLY.SPEC]
This section covers the types of things one can find in the POLY
constructors

If the
MCAR
argument is strictly less than theMCADR
then theTHEN
branch is taken, otherwise theELSE
branch is taken.
12.2 Polynomial API
[in package GEB.POLY.MAIN]
This covers the polynomial API
[method] GAPPLY (MORPHISM <POLY>) OBJECT
My main documentation can be found on
GAPPLY
I am the
GAPPLY
forPOLY:<POLY>
, theOBJECT
that I expect is of typeNUMBER
.GAPPLY
reduces down to ordinary common lisp expressions rather straight forwardlySome examples of me are
(inpackage :geb.poly) POLY> (gapply (ifzero ( ident ident 1) 10 ident) 5) 5 (3 bits, #x5, #o5, #b101) POLY> (gapply (ifzero ( ident ident) 10 ident) 5) 10 (4 bits, #xA, #o12, #b1010) POLY> (gapply ( (* 2 ident ident) (* ident ident)) 5) 25 (5 bits, #x19, #o31, #b11001)
[method] GAPPLY (MORPHISM INTEGER) OBJECT
My main documentation can be found on
GAPPLY
I am the
GAPPLY
forINTEGER
s, theOBJECT
that I expect is of typeNUMBER
. I simply return myself.Some examples of me are
(inpackage :geb.poly) POLY> (gapply 10 5) 10 (4 bits, #xA, #o12, #b1010)
12.3 Polynomial Constructors
[in package GEB.POLY.SPEC]
Every accessor for each of the CLASS
's found here are from Accessors
[function] + MCAR MCADR &REST ARGS
Creates a multiway constructor for +
[function] * MCAR MCADR &REST ARGS
Creates a multiway constructor for *
[function] / MCAR MCADR &REST ARGS
Creates a multiway constructor for /
[function]  MCAR MCADR &REST ARGS
Creates a multiway constructor for 
[function] MOD MCAR MCADR
MOD
ARG1 by ARG2
[function] COMPOSE MCAR MCADR &REST ARGS
Creates a multiway constructor for
COMPOSE
[function] IFZERO PRED THEN ELSE
checks if
PREDICATE
is zero then take theTHEN
branch otherwise theELSE
branch
[function] IFLT MCAR MCADR THEN ELSE
Checks if the
MCAR
is less than theMCADR
and chooses the appropriate branch
12.4 Polynomial Transformations
[in package GEB.POLY.TRANS]
This covers transformation functions from
[method] TOCIRCUIT (MORPHISM <POLY>) NAME
Turns a
POLY
term into a VampIR Gate with the given name
[method] TOVAMPIR (OBJ INTEGER) VALUE LETVARS
Numbers act like a constant function, ignoring input
[method] TOVAMPIR (OBJ IFZERO) VALUE LETVARS
The
PREDICATE
that comes in must be 1 or 0 for the formula to work out.
13 The Simply Typed Lambda Calculus model
[in package GEB.LAMBDA]
This covers GEB's view on simply typed lambda calculus
This serves as a useful frontend for those wishing to write a compiler to GEB and do not wish to target the categorical model.
If one is targeting their compiler to the frontend, then the following code should be useful for you.
(inpackage :geb.lambda.main)
MAIN>
(tocircuit
(lamb (list (coprod so1 so1))
(index 0))
:id)
(def id x1 = {
(x1)
};)
MAIN>
(tocircuit
(lamb (list (coprod so1 so1))
(caseon (index 0)
(lamb (list so1)
(right so1 (unit)))
(lamb (list so1)
(left so1 (unit)))))
:not)
(def not x1 = {
(((1  x1) * 1) + (x1 * 0), ((1  x1) * 1) + (x1 * 0))
};)
MAIN> (tocircuit (lamb (list gebbool:bool)
(left so1 (right so1 (index 0)))) :foo)
(def foo x1 = {
(0, 1, x1)
};)
For testing purposes, it may be useful to go to the BITC
backend and
run our interpreter
MAIN>
(gapply (tobitc
(lamb (list (coprod so1 so1))
(caseon (index 0)
(lamb (list so1)
(right so1 (unit)))
(lamb (list so1)
(left so1 (unit))))))
#*1)
#*00
MAIN>
(gapply (tobitc
(lamb (list (coprod so1 so1))
(caseon (index 0)
(lamb (list so1)
(right so1 (unit)))
(lamb (list so1)
(left so1 (unit))))))
#*0)
#*11
13.1 Lambda Specification
[in package GEB.LAMBDA.SPEC]
This covers the various the abstract data type that is the simply
typed lambda calculus within GEB. The class presents untyped STLC
terms.

Type of untyped terms of
STLC
. Each class of a term has a slot for a type, which can be filled by auxillary functions or by user. Types are represented as SUBSTOBJ.
[class] <STLC> DIRECTPOINTWISEMIXIN METAMIXIN CATOBJ
Class of untyped terms of simply typed lambda claculus. Given our presentation, we look at the latter as a type theory spanned by empty, unit types as well as coproduct, product, and function types.

The
ABSURD
term provides an element of an arbitrary type given a term of the empty type, denoted by SO0. The formal grammar ofABSURD
is(absurd tcod term)
where we possibly can include type information by
(absurd tcod term :ttype ttype)
The intended semantics are:
TCOD
is a type whose term we want to get (and hence a SUBSTOBJ) andTERM
is a term of the empty type (and hence anSTLC
.This corresponds to the elimination rule of the empty type. Namely, given $$\Gamma \vdash \text{tcod : Type}$$ and $$\Gamma \vdash \text{term : so0}$$ one deduces $$\Gamma \vdash \text{(absurd tcod term) : tcod}$$

The unique term of the unit type, the latter represented by SO1. The formal grammar of
UNIT
is(unit)
where we can optionally include type information by
(unit :ttype ttype)
Clearly the type of
UNIT
is SO1 but here we provide all terms untyped.This grammar corresponds to the introduction rule of the unit type. Namely $$\Gamma \dashv \text{(unit) : so1}$$

Term of a coproduct type gotten by injecting into the left type of the coproduct. The formal grammar of
LEFT
is(left rty term)
where we can include optional type information by
(left rty term :ttype ttype)
The indended semantics are as follows:
RTY
should be a type (and hence a SUBSTOBJ) and specify the right part of the coproduct of the typeTTYPE
of the entire term. The term (and hence anSTLC
) we are injecting isTERM
.This corresponds to the introduction rule of the coproduct type. Namely, given $$\Gamma \dashv \text{(ttype term) : Type}$$ and $$\Gamma \dashv \text{rty : Type}$$ with $$\Gamma \dashv \text{term : (ttype term)}$$ we deduce $$\Gamma \dashv \text{(left rty term) : (coprod (ttype term) rty)}$$

Term of a coproduct type gotten by injecting into the right type of the coproduct. The formal grammar of
RIGHT
is(right lty term)
where we can include optional type information by
(right lty term :ttype ttype)
The indended semantics are as follows:
LTY
should be a type (and hence a SUBSTOBJ) and specify the left part of the coproduct of the typeTTYPE
of the entire term. The term (and hence anSTLC
) we are injecting isTERM
.This corresponds to the introduction rule of the coproduct type. Namely, given $$\Gamma \dashv \text{(ttype term) : Type}$$ and $$\Gamma \dashv \text{lty : Type}$$ with $$\Gamma \dashv \text{term : (ttype term)}$$ we deduce $$\Gamma \dashv \text{(right lty term) : (coprod lty (ttype term))}$$

A term of an arbutrary type provided by casing on a coproduct term. The formal grammar of
CASEON
is(caseon on ltm rtm)
where we can possibly include type information by
(caseon on ltm rtm :ttype ttype)
The intended semantics are as follows:
ON
is a term (and hence anSTLC
) of a coproduct type, andLTM
andRTM
terms (hence alsoSTLC
) of the same type in the context of  appropriately  (mcar (ttype on)) and (mcadr (ttype on)).This corresponds to the elimination rule of the coprodut type. Namely, given $$\Gamma \vdash \text{on : (coprod (mcar (ttype on)) (mcadr (ttype on)))}$$ and $$\text{(mcar (ttype on))} , \Gamma \vdash \text{ltm : (ttype ltm)}$$ , $$\text{(mcadr (ttype on))} , \Gamma \vdash \text{rtm : (ttype ltm)}$$ we get $$\Gamma \vdash \text{(caseon on ltm rtm) : (ttype ltm)}$$ Note that in practice we append contexts on the left as computation of
INDEX
is done from the left. Otherwise, the rules are the same as in usual type theory if context was read from right to left.

A term of the product type gotten by pairing a terms of a left and right parts of the product. The formal grammar of
PAIR
is(pair ltm rtm)
where we can possibly include type information by
(pair ltm rtm :ttype ttype)
The intended semantics are as follows:
LTM
is a term (and hence anSTLC
) of a left part of the product type whose terms we are producing.RTM
is a term (hence alsoSTLC
)of the right part of the product.The grammar corresponds to the introdcution rule of the pair type. Given $$\Gamma \vdash \text{ltm : (mcar (ttype (pair ltm rtm)))}$$ and $$\Gamma \vdash \text{rtm : (mcadr (ttype (pair ltm rtm)))}$$ we have $$\Gamma \vdash \text{(pair ltm rtm) : (ttype (pair ltm rtm))}$$

The first projection of a term of a product type. The formal grammar of
FST
is:(fst term)
where we can possibly include type information by
(fst term :ttype ttype)
The indended semantics are as follows:
TERM
is a term (and hence anSTLC
) of a product type, to whose left part we are projecting to.This corresponds to the first projection function gotten by induction on a term of a product type.

The second projection of a term of a product type. The formal grammar of
SND
is:(snd term)
where we can possibly include type information by
(snd term :ttype ttype)
The indended semantics are as follows:
TERM
is a term (and hence anSTLC
) of a product type, to whose right part we are projecting to.This corresponds to the second projection function gotten by induction on a term of a product type.

A term of a function type gotten by providing a term in the codomain of the function type by assuming one is given variables in the specified list of types.
LAMB
takes in theTDOM
accessor a list of types  and hence of SUBSTOBJ  and in theTERM
a term  and hence anSTLC
. The formal grammar ofLAMB
is:(lamb tdom term)
where we can possibly include type information by
(lamb tdom term :ttype ttype)
The intended semnatics are:
TDOM
is a list of types (and hence a list of SUBSTOBJ) whose iterative product of components form the domain of the function type.TERM
is a term (and hence anSTLC
) of the codomain of the function type gotten in the context to whom we append the list of the domains.For a list of length 1, corresponds to the introduction rule of the function type. Namely, given $$\Gamma \vdash \text{tdom : Type}$$ and $$\Gamma, \text{tdom} \vdash \text{term : (ttype term)}$$ we have $$\Gamma \vdash \text{(lamb tdom term) : (sohomobj tdom (ttype term))}$$
For a list of length n, this coreesponds to the iterated lambda type, e.g.
(lamb (list so1 so0) (index 0))
is a term of
(sohomobj (prod so1 so0) so0)
or equivalently
(sohomobj so1 (sohomobj so0 so0))
due to Geb's computational definition of the function type.
Note that
INDEX
0 in the above code is of type SO1. So that after annotating the term, one getsLAMBDA> (ttype (term (lamb (list so1 so0)) (index 0))) s1
So the counting of indeces starts with the leftmost argument for computational reasons. In practice, typing of
LAMB
corresponds with taking a list of arguments provided to a lambda term, making it a context in that order and then counting the index of the varibale. Typetheoretically,$$\Gamma \vdash \lambda \Delta (index i)$$ $$\Delta, \Gamma \vdash (index i)$$
So that by the operational semantics of
INDEX
, the type of (index i) in the above context will be the i'th element of the Delta context counted from the left. Note that in practice we append contexts on the left as computation ofINDEX
is done from the left. Otherwise, the rules are the same as in usual type theory if context was read from right to left.

A term of an arbitrary type gotten by applying a function of an iterated function type with a corresponding codomain iteratively to terms in the domains.
APP
takes as argument for theFUN
accessor a function  and hence anSTLC
 whose function type has domain an iteratedGEB:PROD
of SUBSTOBJ and for theTERM
a list of terms  and hence ofSTLC
 matching the types of the product. The formal grammar ofAPP
is(app fun term)
where we can possibly include type information by
(app fun term :ttype ttype)
The intended semantics are as follows:
FUN
is a term (and hence anSTLC
) of a coproduct type  say of (sohomobj (ttype term) y)  andTERM
is a list of terms (hence also ofSTLC
) with nth term in the list having the nth part of the function type.For a oneargument term list, this corresponds to the elimination rule of the function type. Given $$\Gamma \vdash \text{fun : (sohomobj (ttype term) y)}$$ and $$\Gamma \vdash \text{term : (ttype term)}$$ we get $$\Gamma \vdash \text{(app fun term) : y}$$
For several arguments, this corresponds to successive function application. Using currying, this corresponds to, given
G ⊢ (sohomobj (A₁ × ··· × Aₙ₋₁) Aₙ) G ⊢ f : (sohomobj (A₁ × ··· × Aₙ₋₁) G ⊢ tᵢ : Aᵢ
then for each
i
less thann
gets usG ⊢ (app f t₁ ··· tₙ₋₁) : Aₙ
Note again that i'th term should correspond to the ith element of the product in the codomain counted from the left.

The variable term of an arbitrary type in a context. The formal grammar of
INDEX
is(index pos)
where we can possibly include type information by
(index pos :ttype ttype)
The intended semantics are as follows:
POS
is a natural number indicating the position of a type in a context.This corresponds to the variable rule. Namely given a context $$\Gamma_1 , \ldots , \Gamma_{pos} , \ldots , \Gamma_k $$ we have
$$\Gamma_1 , \ldots , \Gamma_k \vdash \text{(index pos) :} \Gamma_{pos}$$
Note that we add contexts on the left rather than on the right contra classical typetheoretic notation.

An error term of a type supplied by the user. The formal grammar of
ERR
is(err ttype)
The intended semantics are as follows:
ERR
represents an error node currently having no particular feedback but with functionality to be of an arbitrary type. Note that this is the onlySTLC
term class which does not haveTTYPE
a possibly empty accessor.

A term representing syntactic summation of two bits of the same width. The formal grammar of
PLUS
is(plus ltm rtm)
where we can possibly supply typing info by
(plus ltm rtm :ttype ttype)
Note that the summation is ranged, so if the operation goes above the bitsize of supplied inputs, the corresponding VampIR code will not verify.

A term representing syntactic multiplication of two bits of the same width. The formal grammar of
TIMES
is(times ltm rtm)
where we can possibly supply typing info by
(times ltm rtm :ttype ttype)
Note that the multiplication is ranged, so if the operation goes above the bitsize of supplied inputs, the corresponding VampIR code will not verify.

A term representing syntactic subtraction of two bits of the same width. The formal grammar of
MINUS
is(minus ltm rtm)
where we can possibly supply typing info by
(minus ltm rtm :ttype ttype)
Note that the subtraction is ranged, so if the operation goes below zero, the corresponding VampIR code will not verify.

A term representing syntactic division (floored) of two bits of the same width. The formal grammar of
DIVIDE
is(minus ltm rtm)
where we can possibly supply typing info by
(minus ltm rtm :ttype ttype)

A term representing a choice of a bit. The formal grammar of
BITCHOICE
is(bitchoice bitv)
where we can possibly supply typing info by
(bitchoice bitv :ttype ttype)
Note that the size of bits matter for the operations one supplies them to. E.g. (plus (bitchoice #1) (bitchoice #00)) is not going to pass our typecheck, as both numbers ought to be of exact same bitwidth.

lambeq predicate takes in two bit inputs of same bitwidth and gives true if they are equal and false otherwise. Note that for the usual VampIR code interpretations, that means that we associate true with left input into bool and false with the right. Appropriately, in VampIR the first branch will be associated with the 0 input and teh second branch with 1.

lamblt predicate takes in two bit inputs of same bitwidth and gives true if ltm is less than rtm and false otherwise. Note that for the usual VampIR code interpretations, that means that we associate true with left input into bool and false with the right. Appropriately, in VampIR the first branch will be associated with the 0 input and teh second branch with 1.

A term representing syntactic modulus of the first number by the second number. The formal grammar of
MODULO
is(modulo ltm rtm)
where we can possibly supply typing info by
(modulo ltm rtm :ttype ttype)
meaning that we take ltm mod rtm
 [function] ABSURD TCOD TERM &KEY (TTYPE
NIL
)
 [function] UNIT &KEY (TTYPE
NIL
)
 [function] LEFT RTY TERM &KEY (TTYPE
NIL
)
 [function] RIGHT LTY TERM &KEY (TTYPE
NIL
)
 [function] CASEON ON LTM RTM &KEY (TTYPE
NIL
)
 [function] PAIR LTM RTM &KEY (TTYPE
NIL
)
 [function] FST TERM &KEY (TTYPE
NIL
)
 [function] SND TERM &KEY (TTYPE
NIL
)
 [function] LAMB TDOM TERM &KEY (TTYPE
NIL
)
 [function] APP FUN TERM &KEY (TTYPE
NIL
)
 [function] INDEX POS &KEY (TTYPE
NIL
)
 [function] ERR TTYPE
 [function] PLUS LTM RTM &KEY (TTYPE
NIL
)
 [function] TIMES LTM RTM &KEY (TTYPE
NIL
)
 [function] MINUS LTM RTM &KEY (TTYPE
NIL
)
 [function] DIVIDE LTM RTM &KEY (TTYPE
NIL
)
 [function] BITCHOICE BITV &KEY (TTYPE
NIL
)
 [function] LAMBEQ LTM RTM &KEY (TTYPE
NIL
)
 [function] LAMBLT LTM RTM &KEY (TTYPE
NIL
)
 [function] ABSURD TCOD TERM &KEY (TTYPE
NIL
)
Accessors of ABSURD
Accessors of UNIT
Accessors of LEFT
Accessors of RIGHT
Accessors of CASEON
Accessors of PAIR
Accessors of FST
Accessors of SND
Accessors of LAMB
Accessors of APP
Accessors of INDEX
Accessor of ERR
Accessors of PLUS
Accessors of TIMES
Accessors of MINUS
Accessors of DIVIDE
Accessors of BITCHOICE
Accessors of LAMBEQ
Accessors of LAMBLT
Accessors of MODULO
 [genericfunction] ON OBJ
13.2 Main functionality
[in package GEB.LAMBDA.MAIN]
This covers the main API for the STLC
module
[genericfunction] ANNTERM1 CTX TTERM
Given a list of
SUBSTOBJ
objects withSOHOMOBJ
occurences replaced byFUNTYPE
and anSTLC
similarly replacing type occurences of the hom object toFUNTYPE
, provides theTTYPE
accessor to all subterms as well as the term itself, usingFUNTYPE
. Once again, note that it is important for the context and term to be giving as per above description. While not always, not doing so result in an error upon evaluation. As an example of a valid entry we have(annterm1 (list so1 (funtype so1 so1)) (app (index 1) (list (index 0))))
while
(annterm1 (list so1 (sohomobj so1 so1)) (app (index 1) (list (index 0))))
produces an error trying to use. This warning applies to other functions taking in context and terms below as well.
Moreover, note that for terms whose typing needs addition of new context we append contexts on the left rather than on the right contra usual type theoretic notation for the convenience of computation. That means, e.g. that asking for a type of a lambda term as below produces:
LAMBDA> (ttype (term (annterm1 (lambda (list so1 so0) (index 0))))) s1
as we count indeces from the left of the context while appending new types to the context on the left as well. For more info check
LAMB
[function] INDEXCHECK I CTX
Given an natural number
I
and a context, checks that the context is of length at leastI
and then produces the Ith entry of the context counted from the left starting with 0.

Given a
SUBSTOBJ
whose subobjects might have aFUNTYPE
occurence replaces all occurences ofFUNTYPE
with a suitableSOHOMOBJ
, hence giving a pureSUBSTOBJ
LAMBDA> (funtohom (funtype gebbool:bool gebbool:bool)) (× (+ GEBBOOL:FALSE GEBBOOL:TRUE) (+ GEBBOOL:FALSE GEBBOOL:TRUE))
[function] ANNTERM2 TTERM
Given an
STLC
term with aTTYPE
accessor fromANNTERM1
 i.e. including possibleFUNTYPE
occurences  reannotates the term and its subterms with actualSUBSTOBJ
objects.
[function] ANNOTATEDTERM CTX TERM
Given a context consisting of a list of
SUBSTOBJ
with occurences ofSOHOMOBJ
replaced byFUNTYPE
and anSTLC
term with similarly replaced occurences ofSOHOMOBJ
, provides anSTLC
with all subterms typed, i.e. providing theTTYPE
accessor, which is a pureSUBSTOBJ
[function] TYPEOFTERMWFUN CTX TTERM
Given a context consisting of a list of
SUBSTOBJ
with occurences ofSOHOMOBJ
replaced byFUNTYPE
and anSTLC
term with similarly replaced occurences ofSOHOMOBJ
, gives out a type of the whole term with occurences ofSOHOMOBJ
replaced byFUNTYPE
.
[function] TYPEOFTERM CTX TTERM
Given a context consisting of a list of
SUBSTOBJ
with occurences ofSOHOMOBJ
replaced byFUNTYPE
and anSTLC
term with similarly replaced occurences ofSOHOMOBJ
, provides the type of the whole term, which is a pureSUBSTOBJ
.
[genericfunction] WELLDEFP CTX TTERM
Given a context consisting of a list of
SUBSTOBJ
with occurences ofSOHOMOBJ
replaced byFUNTYPE
and anSTLC
term with similarly replaced occurences ofSOHOMOBJ
, checks that the term is welldefined in the context based on structural rules of simply typed lambda calculus. returns the t if it is, otherwise returning nil
[class] FUNTYPE DIRECTPOINTWISEMIXIN CATOBJ
Standin for the
SOHOMOBJ
object. It does not have any computational properties and can be seen as just a function of two arguments with accessorsMCAR
to the first argument andMCADR
to the second argument. There is an evident canonical way to associateFUNTYPE
andSOHOMOBJ
pointwise.
 [function] FUNTYPE MCAR MCADR
[function] ERRORP TTERM
Evaluates to true iff the term has an error subterm.
[function] REDUCER TTERM
Reduces a given Lambda term by applying explict betareduction when possible alongside arithmetic simplification. We assume that the lambda and app terms are 1argument
13.3 Transition Functions
[in package GEB.LAMBDA.TRANS]
These functions deal with transforming the data structure to other data types
One important note about the lambda conversions is that all
transition functions except TOCAT
do not take a context.
Thus if the <STLC>
term contains free variables, then call
TOCAT
and give it the desired context before calling
any other transition functions
[method] TOCAT CONTEXT (TTERM <STLC>)
Compiles a checked term in said context to a Geb morphism. If the term has an instance of an erorr term, wraps it in a Maybe monad, otherwise, compiles according to the term model interpretation of
STLC

I convert a lambda term into a
GEB.POLY.SPEC:POLY
termNote that
<STLC>
terms with free variables require a context, and we do not supply them here to conform to the standard interfaceIf you want to give a context, please call tocat before calling me

I convert a lambda term into a
GEB.BITC.SPEC:BITC
termNote that
<STLC>
terms with free variables require a context, and we do not supply them here to conform to the standard interfaceIf you want to give a context, please call tocat before calling me

I convert a lambda term into a
GEB.SEQN.SPEC:SEQN
termNote that
<STLC>
terms with free variables require a context, and we do not supply them here to conform to the standard interfaceIf you want to give a context, please call tocat before calling me
[method] TOCIRCUIT (OBJ <STLC>) NAME
I convert a lambda term into a vampir term
Note that
<STLC>
terms with free variables require a context, and we do not supply them here to conform to the standard interfaceIf you want to give a context, please call tocat before calling me
13.3.1 Utility Functionality
These are utility functions relating to translating lambda terms to other types
[function] STLCCTXTOMU CONTEXT
Converts a generic (CODE
) context into aSUBSTMORPH
. Note that usually contexts can be interpreted in a category as a $Sigma$type$, which in a nondependent setting gives us a usualPROD
LAMBDA> (stlcctxtomu (list so1 (funtohom (funtype gebbool:bool gebbool:bool)))) (× s1 (× (+ GEBBOOL:FALSE GEBBOOL:TRUE) (+ GEBBOOL:FALSE GEBBOOL:TRUE)) s1)
[function] SOHOM DOM COD
Computes the homobject of two
SUBSTMORPH
s
14 Mixins
[in package GEB.MIXINS]
Various mixins of the project. Overall all these offer various services to the rest of the project
14.1 Pointwise Mixins
Here we provide various mixins that deal with classes in a pointwise
manner. Normally, objects can not be compared in a pointwise manner,
instead instances are compared. This makes functional idioms like
updating a slot in a pure manner (allocating a new object), or even
checking if two objects are EQUAL
able adhoc. The pointwise API,
however, derives the behavior and naturally allows such idioms

Provides the service of giving point wise operations to classes
Further we may wish to hide any values inherited from our superclass due to this we can instead compare only the slots defined directly in our class
[class] DIRECTPOINTWISEMIXIN POINTWISEMIXIN
Works like
POINTWISEMIXIN
, however functions onPOINTWISEMIXIN
will only operate on directslots instead of all slots the class may contain.Further all
DIRECTPOINTWISEMIXIN
's arePOINTWISEMIXIN
's
14.2 Pointwise API
These are the general API functions on any class that have the
POINTWISEMIXIN
service.
Functions like TOPOINTWISELIST
allow generic list traversal APIs to
be built off the keyvalue pair of the raw object form, while
OBJEQUALP
allows the checking of functional equality between
objects. Overall the API is focused on allowing more generic
operations on classes that make them as useful for generic data
traversal as LIST
(0
1
)'s are
[genericfunction] TOPOINTWISELIST OBJ
Turns a given object into a pointwise
LIST
(0
1
). listing theKEYWORD
slotname next to their value.
[genericfunction] OBJEQUALP OBJECT1 OBJECT2
Compares objects with pointwise equality. This is a much weaker form of equality comparison than
STANDARDOBJECT
EQUALP
, which does the much stronger pointer quality
[genericfunction] POINTWISESLOTS OBJ
Works like
C2MOP:COMPUTESLOTS
however on the object rather than the class
 [function] MAPPOINTWISE FUNCTION OBJ
 [function] REDUCEPOINTWISE FUNCTION OBJ INITIAL
14.3 Mixins Examples
Let's see some example uses of POINTWISEMIXIN
:
(objequalp (geb:terminal geb:so1)
(geb:terminal geb:so1))
=> t
(topointwiselist (geb:coprod geb:so1 geb:so1))
=> ((:MCAR . s1) (:MCADR . s1))
14.4 Metadata Mixin
Metadata is a form of meta information about a particular object. Having metadata about an object may be useful if the goal requires annotating some data with type information, identification information, or even various levels of compiler information. The possibilities are endless and are a standard technique.
For this task we offer the METAMIXIN
which will allow
metadata to be stored for any type that uses its service.

Use my service if you want to have metadata capabilities associated with the given object. Performance covers my performance characteristics
For working with the structure it is best to have operations to treat it like an ordinary hashtable
[function] METAINSERT OBJECT KEY VALUE &KEY WEAK
Inserts a value into storage. If the key is a one time object, then the insertion is considered to be volatile, which can be reclaimed when no more references to the data exists.
If the data is however a constant like a string, then the insertion is considered to be long lived and will always be accessible
The :weak keyword specifies if the pointer stored in the value is weak
[function] METALOOKUP OBJECT KEY
Lookups the requested key in the metadata table of the object. We look past weak pointers if they exist
14.4.1 Performance
The data stored is at the CLASS
level. So having your type take the
METAMIXIN
does interfere with the cache.
Due to concerns about meta information being populated over time, the table which it is stored with is in a weak hashtable, so if the object that the metadata is about gets deallocated, so does the metadata table.
The full layout can be observed from this interaction
;; any class that uses the service
(defparameter *x* (makeinstance 'metamixin))
(metainsert *x* :a 3)
(defparameter *y* (makeinstance 'metamixin))
(metainsert *y* :b 3)
(defparameter *z* (makeinstance 'metamixin))
;; where {} is a hashtable
{*x* {:a 3}
*y* {:b 3}}
Since *z*
does not interact with storage no overhead of storage is
had. Further if `x goes out of scope, gc would reclaim the table leaving
{*y* {:b 3}}
for the hashtable.
Even the tables inside each object's map are weak, thus we can make storage inside metadata be separated into volatile and stable storage.
15 Geb Utilities
[in package GEB.UTILS]
The Utilities package provides general utility functionality that is used throughout the GEB codebase

Allows us to state a list contains a given type.
NOTE
This does not type check the whole list, but only the first element. This is an issue with how lists are defined in the language. Thus this should be be used for intent purposes.
For a more proper version that checks all elements please look at writing code like
(deftype normalformlist () `(satisfies normalformlist)) (defun normalformlist (list) (and (listp list) (every (lambda (x) (typep x 'normalform)) list))) (deftype normalform () `(or wire constant))
Example usage of this can be used with
typep
(typep '(1 . 23) '(listof fixnum)) => NIL (typep '(1 23) '(listof fixnum)) => T (typep '(1 3 4 "hi" 23) '(listof fixnum)) => T (typep '(1 23 . 5) '(listof fixnum)) => T
Further this can be used in type signatures
(> foo (fixnum) (listof fixnum)) (defun foo (x) (list x))
[function] SYMBOLTOKEYWORD SYMBOL
[macro] MUFFLEPACKAGEVARIANCE &REST PACKAGEDECLARATIONS
Muffle any errors about package variance and stating exports out of order. This is particularly an issue for SBCL as it will error when using MGLPAX to do the export instead of
DEFPACKAGE
.This is more modular thank MGLPAX:DEFINEPACKAGE in that this can be used with any package creation function like UIOP:DEFINEPACKAGE.
Here is an example usage:
(geb.utils:mufflepackagevariance (uiop:definepackage #:geb.lambda.trans (:mix #:trivia #:geb #:serapeum #:commonlisp) (:export :compilecheckedterm :stlcctxtomu)))
[function] SUBCLASSRESPONSIBILITY OBJ
Denotes that the given method is the subclasses responsibility. Inspired from Smalltalk
 [function] SHALLOWCOPYOBJECT ORIGINAL
[genericfunction] COPYINSTANCE OBJECT &REST INITARGS &KEY &ALLOWOTHERKEYS
Makes and returns a shallow copy of
OBJECT
.An uninitialized object of the same class as
OBJECT
is allocated by callingALLOCATEINSTANCE
. For all slots returned by CLASSSLOTS, the returned object has the same slot values and slotunbound status asOBJECT
.REINITIALIZEINSTANCE
is called to update the copy withINITARGS
.
[macro] MAKEPATTERN OBJECTNAME &REST CONSTRUCTORNAMES
make pattern matching position style instead of record style. This removes the record constructor style, however it can be brought back if wanted
(defclass alias (<substmorph> <substobj>) ((name :initarg :name :accessor name :type symbol :documentation "The name of the GEB object") (obj :initarg :obj :accessor obj :documentation "The underlying geb object")) (:documentation "an alias for a geb object")) (makepattern alias name obj)
[function] NUMBERTODIGITS NUMBER &OPTIONAL REM
turns an
INTEGER
into a list of its digits
[function] DIGITTOUNDER DIGIT
Turns a digit into a subscript string version of the number
[function] NUMBERTOUNDER INDEX
[function] APPLYN TIMES F INITIAL
Applies a function, f, n
TIMES
to theINITIAL
valuesGEB> (applyn 10 #'1+ 0) 10 (4 bits, #xA, #o12, #b1010)
15.1 Accessors
These functions are generic lenses of the GEB codebase. If a class is defined, where the names are not known, then these accessors are likely to be used. They may even augment existing classes.

Grabs the underlying object

the name of the given object

the function of the object
[genericfunction] PREDICATE OBJ
the
PREDICATE
of the object

the then branch of the object

the then branch of the object

the code of the object
16 Testing
[in package GEBTEST]
We use parachute as our testing framework.
Please read the manual for extra features and how to better lay out future tests
[function] RUNTESTS &KEY (INTERACTIVE?
NIL
) (SUMMARY?NIL
) (PLAIN?T
) (DESIGNATORS '(GEBTESTSUITE
))Here we run all the tests. We have many flags to determine how the tests ought to work
(runtests :plain? nil :interactive? t) ==> 'interactive (runtests :summary? t :interactive? t) ==> 'noisysummary (runtests :interactive? t) ==> 'noisyinteractive (runtests :summary? t) ==> 'summary (runtests) ==> 'plain (runtests :designators '(geb geb.lambda)) ==> run only those packages
[function] CODECOVERAGE &OPTIONAL (PATH
NIL
)generates code coverage, for CCL the coverage can be found at
simply run this function to generate a fresh one