Added Bitc polynomial backend and transformation to vampir

Adds category of boolean circuits (BITC). The objects in this category
are just natural numbers representing the type of bit vectors of a
certain length. There are nine methods for constructing morphisms;

- (compose x y), which composes morphisms x and y.
- (ident n), which is the identity on n.
- (fork n), which maps n onto 2*n by copying its inputs.
- (parallel x y), which (if x : a -> b and y : c -> d) will be a
  morphism from a + c -> b + d, running x and y on subvectors.
- (swap n m), which maps n + m onto m + n by swapping.
- ONE, which represents the map from 0 onto 1 producing a vector with only 1 in it.
- ZERO, which represents the map from 0 onto 1 producing a vector with only 0 in it.
- (drop n), which represents the unique morphism from n to 0.
- (branch x y), which (if x : a -> b and y : a -> b) maps 1+a to b by
  splitting on the first bit to decide which morphism to apply to the
  remaining bits.

There are other ways to formulate this category, but I think this
particular formulation is quite convenient.

I've implemented a `to-bitc` function in geb.trans which translates
geb objects and morphisms into bitc objects and
morphisms. Additionally, I've implemented a `to-vampir` function in
bitc.trans which translates a bit morphism into a vampire morphism.

I'm not sure what else is needed, but the core implementation is done
for now. In the future, this should be extended to a category whose
objects represent vectors over some finite set other than the
booleans. The reason I didn't do that hear is because coproducts are
only binary and there aren't finite sets beyond so0 and so1, so
bitvectors are quite natural and using anything else would require
post-hoc optimization, but future versions of geb may want more. Also,
I'd like to know what, if any, performance benefits this gives over
the univariate polynomial formulation. I didn't test that.

docs/documentation.lisp

@@ -12,6 +12,7 @@
   (@idioms           pax:section)
   (@geb              pax:section)
   (@geb-gui-manual   pax:section)
+  (@bitc-manual      pax:section)
   (@poly-manual      pax:section)
   (@stlc             pax:section)
   (@mixins           pax:section)

docs/package.lisp

@@ -5,6 +5,7 @@
   (:import-from #:geb.utils  #:@geb-utils-manual)
   (:import-from #:geb-test   #:@geb-test-manual)
   (:import-from #:geb.poly   #:@poly-manual)
+  (:import-from #:geb.bitc   #:@bitc-manual)
   (:import-from #:geb.specs  #:@geb-specs)
   (:import-from #:geb.entry  #:@geb-entry)
   (:import-from #:geb.lambda #:@stlc)

geb.asd

@@ -9,11 +9,15 @@
   :description "Gödel, Escher, Bach, a categorical view of computation"
   :build-pathname "../build/geb.image"
   :entry-point "geb.entry::entry"
+
   :build-operation "program-op"
   :author "Mariari"
+
   :license "MIT"
+
   :pathname "src/"
   :components
+
   ((:module util
     :serial t
     :description "Internal utility functions"
@@ -46,6 +50,12 @@
     :description "Polynomial"
     :depends-on (util geb vampir specs)
     :components ((:file package)))
+   (:module bitc
+    :serial t
+    :description "bitc (Boolean Circuits)"
+    :depends-on (util vampir mixins specs)
+    :components ((:file package)
+                 (:file bitc)))
    (:module lambda
     :serial t
     :depends-on (geb specs)
@@ -68,6 +78,8 @@
                  (:file lambda)
                  (:file poly)
                  (:file poly-printer)
+                 (:file bitc)
+                 (:file bitc-printer)
                  ;; HACK: to make the package properly refer to the
                  ;; right symbols
                  (:file ../util/package)))
@@ -81,11 +93,12 @@
     :pathname "../src/"
     :components ((:file lambda/trans)
                  (:file geb/trans)
-                 (:file poly/trans)))
+                 (:file poly/trans)
+                 (:file bitc/trans)))
    (:module entry
     :serial t
     :description "Entry point for the geb codebase"
-    :depends-on (util geb vampir specs poly lambda)
+    :depends-on (util geb vampir specs poly bitc lambda)
     :components ((:file package)
                  (:file entry))))
   :in-order-to ((asdf:test-op (asdf:test-op :geb/test))))
@@ -124,6 +137,7 @@
    (:file lambda)
    (:file lambda-conversion)
    (:file poly)
+   (:file bitc)
    (:file pipeline)
    (:module gui
     :serial t

src/bitc/bitc.lisp

@@ -0,0 +1,33 @@
+(in-package :geb.bitc.main)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Domain and codomain definitions
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(defmethod dom ((x <bitc>))
+  (typecase-of bitc x
+    (compose  (dom (mcadr x)))
+    (fork     (mcar x))
+    (parallel (+ (dom (mcar x)) (dom (mcadr x))))
+    (swap     (+ (mcar x) (mcadr x)))
+    (one      0)
+    (zero     0)
+    (ident    (mcar x))
+    (drop     (mcar x))
+    (branch   (+ 1 (dom (mcar x))))
+    (otherwise
+      (subclass-responsibility x))))
+
+(defmethod codom ((x <bitc>))
+  (typecase-of bitc x
+    (compose  (codom (mcar x)))
+    (fork     (* 2 (mcar x)))
+    (parallel (+ (codom (mcar x)) (codom (mcadr x))))
+    (swap     (+ (mcar x) (mcadr x)))
+    (one      1)
+    (zero     1)
+    (ident    (mcar x))
+    (drop     0)
+    (branch   (codom (mcar x)))
+    (otherwise
+      (subclass-responsibility x))))

src/bitc/package.lisp

@@ -0,0 +1,54 @@
+(in-package :geb.utils)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;; trans module
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(muffle-package-variance
+ (defpackage #:geb.bitc.trans
+   (:local-nicknames (:vamp :geb.vampir.spec))
+   (:use #:geb.common #:geb.bitc.spec)
+   (:shadowing-import-from #:geb.bitc.spec #:drop #:fork)))
+
+(in-package :geb.bitc.trans)
+
+(pax:defsection @bitc-trans (:title "Bits (Boolean Circuit) Transformations")
+  "This covers transformation functions from"
+  (to-circuit pax:function)
+  (to-vampir  pax:generic-function)
+  (to-vampir  (pax:method () (compose t)))
+  (to-vampir  (pax:method () (fork t)))
+  (to-vampir  (pax:method () (parallel t)))
+  (to-vampir  (pax:method () (swap t)))
+  (to-vampir  (pax:method () (one t)))
+  (to-vampir  (pax:method () (zero t)))
+  (to-vampir  (pax:method () (ident t)))
+  (to-vampir  (pax:method () (drop t)))
+  (to-vampir  (pax:method () (branch t))))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;; bitc module
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(geb.utils:muffle-package-variance
+ (uiop:define-package #:geb.bitc.main
+   (:use #:geb.common #:geb.mixins)
+   (:shadowing-import-from #:geb.bitc.spec #:drop #:fork)
+   (:use-reexport #:geb.bitc.trans #:geb.bitc.spec)))
+
+(geb.utils:muffle-package-variance
+ (uiop:define-package #:geb.bitc
+   (:use #:geb.common)
+   (:shadowing-import-from #:geb.bitc.spec :fork :drop)
+   (:use-reexport #:geb.bitc.trans #:geb.bitc.spec #:geb.bitc.main)))
+
+(in-package :geb.bitc.main)
+
+(in-package :geb.bitc)
+
+(pax:defsection @bitc-manual (:title "Bits (Boolean Circuit) Specification")
+  "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"
+  (@bitc              pax:section)
+  (@bitc-constructors pax:section)
+  (@bitc-trans        pax:section))

src/bitc/trans.lisp

@@ -0,0 +1,89 @@
+(in-package :geb.bitc.trans)
+
+(defgeneric to-vampir (morphism values)
+  (:documentation "Turns a BITC term into a Vamp-IR term with a given value"))
+
+(defun to-circuit (morphism name)
+  "Turns a BITC term into a Vamp-IR Gate with the given name"
+  (let* ((wire-count (dom morphism))
+         (wires (loop for i from 1 to wire-count
+                      collect (vamp:make-wire :var (intern (format nil "x~a" i)
+                                                           :keyword)))))
+    (vamp:make-alias :name name
+                     :inputs wires
+                     :body (list (vamp:make-tuples :wires (to-vampir morphism wires))))))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Bits to Vampir Implementation
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(defmethod to-vampir ((obj <bitc>) values)
+  (declare (ignore values))
+  (subclass-responsibility obj))
+
+(defun infix-creation (symbol value1 value2)
+  (vamp:make-infix :op symbol
+                   :lhs value1
+                   :rhs value2))
+
+(defmethod to-vampir ((obj compose) values)
+  (to-vampir (mcar obj)
+             (to-vampir (mcadr obj) values)))
+
+(defmethod to-vampir ((obj fork) values)
+  "Copy input n intput bits into 2*n output bits"
+  (append values values))
+
+(defmethod to-vampir ((obj parallel) values)
+  "Take n + m bits, execute car the n bits and cadr on the m bits and
+  concat the results from car and cadr"
+  (let* ((car  (mcar obj))
+         (cadr (mcadr obj))
+         (cx   (dom car))
+         (inp1 (subseq values 0 cx))
+         (inp2 (subseq values cx)))
+    (append (to-vampir car inp1)
+            (to-vampir cadr inp2))))
+
+(defmethod to-vampir ((obj swap) values)
+  "Turn n + m bits into m + n bits by swapping"
+  (let ((n (mcar obj)))
+    (append (subseq values n)
+            (subseq values 0 n))))
+
+(defmethod to-vampir ((obj one) values)
+  "Produce a bitvector of length 1 containing 1"
+  (declare (ignore values))
+  (list (vamp:make-constant :const 1)))
+
+(defmethod to-vampir ((obj zero) values)
+  "Produce a bitvector of length 1 containing 0"
+  (declare (ignore values))
+  (list (vamp:make-constant :const 0)))
+
+(defmethod to-vampir ((obj ident) values)
+  "turn n bits into n bits by doing nothing"
+  values)
+
+(defmethod to-vampir ((obj drop) values)
+  "turn n bits into an empty bitvector"
+  (declare (ignore values))
+  nil)
+
+(defmethod to-vampir ((obj branch) values)
+  "Look at the first bit.
+
+  If its 1, run f on the remaining bits.
+
+  If its 0, run g on the remaining bits."
+  (let ((x (car values))
+        (xs (cdr values))
+        (f (mcar obj))
+        (g (mcadr obj))
+        (one (vamp:make-constant :const 1)))
+    (mapcar (lambda (f-elem g-elem)
+              (infix-creation :+
+                              (infix-creation :* (infix-creation :- one x) f-elem)
+                              (infix-creation :* x g-elem)))
+            (to-vampir f xs)
+            (to-vampir g xs))))

src/entry/package.lisp

@@ -4,6 +4,7 @@
  (defpackage #:geb.entry
    (:documentation "Entry point for the geb codebase")
    (:local-nicknames  (#:poly #:geb.poly)
+                      (#:bitc #:geb.bitc)
                       (:lambda     :geb.lambda))
    (:use #:serapeum #:common-lisp)))
 

src/geb/package.lisp

@@ -6,7 +6,7 @@
  (defpackage #:geb.main
    (:documentation "Gödel, Escher, Bach categorical model")
    (:use #:common-lisp #:serapeum #:geb.mixins #:geb.utils #:geb.spec)
-   (:local-nicknames (#:poly #:geb.poly.spec))
+   (:local-nicknames (#:poly #:geb.poly.spec) (#:bitc #:geb.bitc.spec))
    (:shadowing-import-from #:geb.spec :left :right :prod :case)
    (:export :prod :case :mcar :mcadr :mcaddr :mcdr :name :func :obj :dom :codom)))
 
@@ -48,7 +48,7 @@
  (defpackage #:geb.trans
    (:documentation "Gödel, Escher, Bach categorical model")
    (:use #:common-lisp #:serapeum #:geb.mixins #:geb.utils #:geb.spec #:geb.main)
-   (:local-nicknames (#:poly #:geb.poly.spec))
+   (:local-nicknames (#:poly #:geb.poly.spec) (#:bitc #:geb.bitc.spec))
    (:shadowing-import-from #:geb.spec :left :right :prod :case)
    (:export :prod :case :mcar :mcadr :mcaddr :mcdr :name :func :obj)))
 
@@ -58,7 +58,8 @@
   "These cover various conversions from @GEB-SUBSTMORPH and @GEB-SUBSTMU
 into other categorical data structures."
   (to-poly    pax:generic-function)
-  (to-circuit pax:function))
+  (to-circuit pax:function)
+  (to-bitc    pax:generic-function))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;; bool module