Implementation of Natural Numbers

docs/documentation.lisp

@@ -13,6 +13,7 @@
   (@geb              pax:section)
   (@geb-extensions   pax:section)
   (@geb-gui-manual   pax:section)
+  (@seqn-manual      pax:section)
   (@bitc-manual      pax:section)
   (@poly-manual      pax:section)
   (@stlc             pax:section)

docs/package.lisp

@@ -4,6 +4,7 @@
   (:import-from #:geb.mixins #:@mixins)
   (:import-from #:geb.utils  #:@geb-utils-manual)
   (:import-from #:geb-test   #:@geb-test-manual)
+  (:import-from #:geb.seqn   #:@seqn-manual)
   (:import-from #:geb.poly   #:@poly-manual)
   (:import-from #:geb.bitc   #:@bitc-manual)
   (:import-from #:geb.specs  #:@geb-specs)

geb.asd

@@ -54,7 +54,7 @@
    (:module geb
     :serial t
     :description "The Main Geb Module"
-    :depends-on (util specs)
+    :depends-on (util specs seqn)
     :components ((:file package)
                  (:file geb)
                  (:file bool)
@@ -74,6 +74,13 @@
     :components ((:file package)
                  (:file bitc)
                  (:file trans)))
+   (:module seqn
+    :serial t
+    :description "seqn (Multi-Bit Sequences)"
+    :depends-on (util vampir mixins specs)
+    :components ((:file package)
+                 (:file seqn)
+                 (:file trans)))
    (:module lambda
     :serial t
     :depends-on (geb specs)
@@ -101,6 +108,8 @@
                  (:file extension-printer)
                  (:file bitc)
                  (:file bitc-printer)
+                 (:file seqn)
+                 (:file seqn-printer)
                  ;; HACK: to make the package properly refer to the
                  ;; right symbols
                  (:file ../util/package)))
@@ -111,7 +120,7 @@
    (:module entry
     :serial t
     :description "Entry point for the geb codebase"
-    :depends-on (util geb vampir specs poly bitc lambda)
+    :depends-on (util geb vampir specs poly bitc lambda seqn)
     :components ((:file package)
                  (:file entry))))
   :in-order-to ((asdf:test-op (asdf:test-op :geb/test))))
@@ -153,6 +162,7 @@
    (:file lambda-trans)
    (:file poly)
    (:file bitc)
+   (:file seqn)
    (:file pipeline)
    (:file list)
    (:module gui

src/entry/package.lisp

@@ -5,6 +5,7 @@
    (:documentation "Entry point for the geb codebase")
    (:local-nicknames  (#:poly #:geb.poly)
                       (#:bitc #:geb.bitc)
+                      (#:seqn #:geb.seqn)
                       (:lambda     :geb.lambda))
    (:use #:geb.common)))
 

src/geb/geb.lisp

@@ -11,6 +11,22 @@
                         (curry (right-morph (comp fun (gather fst x y))))))
     (prod         (curry (curry (prod-left-assoc fun))))))
 
+(defmethod curry-prod (fun fst (snd <natobj>))
+  (let ((num (num snd)))
+    (if (= num 1)
+        (pair
+         ;; On the left, see what the morphism does at 0
+         (curry (comp fun
+                      (prod-mor fst
+                                (nat-const 1 0))))
+         ;; On the left, see what the morphism does at 0
+         (curry (comp fun
+                      (prod-mor fst
+                                (nat-const 1 1)))))
+        (curry (comp fun
+                     (prod-mor fst
+                               (nat-concat 1 (1- num))))))))
+
 (defmethod dom ((x <substmorph>))
   (assure cat-obj
     (typecase-of substmorph x
@@ -29,6 +45,19 @@
       (otherwise
        (subclass-responsibility x)))))
 
+(defmethod dom ((x <natmorph>))
+  (cond ((typep x 'nat-concat)      (prod (nat-width (num-left x))
+                                          (nat-width (num-right x))))
+        ((typep x 'nat-const)       so1)
+        ((typep x 'nat-inj)         (nat-width (num x)))
+        ((typep x 'one-bit-to-bool) (nat-width 1))
+        ((typep x 'nat-decompose)   (nat-width (num x)))
+        (t                          (let ((bit (nat-width (num x))))
+                                     (prod bit bit)))))
+
+(defmethod dom ((x <natobj>))
+  x)
+
 (defmethod dom ((ref reference))
   ref)
 
@@ -55,6 +84,28 @@
       (otherwise
        (subclass-responsibility x)))))
 
+(defmethod codom ((x <natmorph>))
+  (typecase-of natmorph x
+    (nat-inj         (nat-width (1+ (num x))))
+    (nat-concat      (nat-width (+ (num-left x) (num-right x))))
+    (one-bit-to-bool (coprod so1 so1))
+    (nat-decompose   (prod (nat-width 1) (nat-width (1- (num x)))))
+    ((or nat-eq
+         nat-lt)
+     (coprod so1 so1))
+    ((or nat-add
+         nat-sub
+         nat-mult
+         nat-div
+         nat-const)
+     (nat-width (num x)))
+    (otherwise
+     (subclass-responsibility x))))
+
+(defmethod codom ((x <natobj>))
+  x)
+
+
 (-> const (cat-morph cat-obj) (or t comp))
 (defun const (f x)
   "The constant morphism.
@@ -155,33 +206,58 @@ u
     (geb:so0          1)
     (geb:so1          1)))
 
-
-(-> so-eval (substobj substobj) substmorph)
-(defun so-eval (x y)
+(defmethod so-eval ((x <substobj>) y)
   (match-of substobj x
     (so0          (comp (init y) (<-right so1 so0)))
     (so1          (<-left y so1))
     ((coprod a b) (comp (mcase (comp (so-eval a y)
-                                     (so-forget-middle (!-> a y) (!-> b y) a))
+                                     (so-forget-middle (so-hom-obj a y) (so-hom-obj b y) a))
                                (comp (so-eval b y)
-                                     (so-forget-first (!-> a y) (!-> b y) b)))
-                        (distribute (prod (!-> a y) (!-> b y)) a b)))
+                                     (so-forget-first (so-hom-obj a y) (so-hom-obj b y) b)))
+                        (distribute (prod (so-hom-obj a y) (so-hom-obj b y)) a b)))
     ((prod a b)   (let ((eyz   (so-eval b y))
                         (exhyz (so-eval a (so-hom-obj b y)))
-                        (hom   (!-> a (so-hom-obj b y))))
+                        (hom   (so-hom-obj a (so-hom-obj b y))))
                     (comp eyz
                           (pair (comp exhyz (so-forget-right hom a b))
                                 (comp (<-right a b)
                                       (<-right hom (prod a b)))))))))
 
-(defun so-hom-obj (x z)
+(defmethod so-eval ((x <natobj>) y)
+  (let ((num (num x)))
+    (if (= num 1)
+        (comp (so-eval (coprod so1 so1)
+                       y)
+              (prod-mor (so-hom-obj x y)
+                        one-bit-to-bool))
+        (comp (so-eval (prod (nat-width 1)
+                             (nat-width (1- num)))
+                       y)
+              (prod-mor (so-hom-obj x y)
+                        (nat-decompose num))))))
+
+(defmethod so-hom-obj ((x <substobj>) z)
   (match-of substobj x
     (so0          so1)
     (so1          z)
     ((coprod x y) (prod (so-hom-obj x z)
                         (so-hom-obj y z)))
     ((prod x y)   (so-hom-obj x (so-hom-obj y z)))))
 
+(defmethod so-hom-obj ((x <natobj>) z)
+  (let ((num (num x))
+        (bool (coprod so1 so1)))
+    (if (= num 1)
+        (so-hom-obj bool
+                    z)
+        ;; The left part of the product is associated with what the
+        ;; function does on 0, right part of what it does on 1
+        ;; using the choice of interpreting false as left and
+        ;; true as right in bool
+        (so-hom-obj  (prod  (nat-width 1)
+                            (nat-width (1- num)))
+                     z))))
+
 (-> so-forget-right (cat-obj cat-obj cat-obj) substmorph)
 (defun so-forget-right (x y z)
   (pair (<-left x (prod y z))
@@ -286,6 +362,9 @@ and [SO0] into Maybe [SO0]"
                               (maybe (mcadr obj)))))
     (otherwise (subclass-responsibility obj))))
 
+(defmethod maybe ((obj <natobj>))
+  (coprod so1 obj))
+
 (defun curry (f)
   "Curries the given object, returns a [cat-morph]
 
@@ -406,6 +485,30 @@ GEB> (gapply geb-bool:and
     (substobj object)
     (otherwise (subclass-responsibility morph))))
 
+(defmethod gapply ((morph <natmorph>) object)
+  (typecase-of natmorph morph
+    (nat-add   (+ (car object) (cadr object)))
+    (nat-mult  (* (car object) (cadr object)))
+    (nat-sub   (- (car object) (cadr object)))
+    (nat-div   (multiple-value-bind (q)
+                   (floor (car object) (cadr object)) q))
+    (nat-const  (pos morph))
+    (nat-inj    object)
+    (nat-concat  (+ (* (expt 2 (num-right morph)) (car object)) (cadr object)))
+    (one-bit-to-bool (if (= object 0)
+                         (left so1)
+                         (right so1)))
+    (nat-decompose (if (>= object  (expt 2 (1- (num morph))))
+                       (list 1 (- object (expt 2 (1- (num morph)))))
+                       (list 0 object)))
+    (nat-eq        (if (= (car object) (cadr object))
+                       (left so1)
+                       (right so1)))
+    (nat-lt        (if (< (car object) (cadr object))
+                       (left so1)
+                       (right so1)))
+    (otherwise (subclass-responsibility morph))))
+
 ;; I believe this is the correct way to use gapply for cat-obj
 (defmethod gapply ((morph cat-obj) object)
   "My main documentation can be found on [GAPPLY][generic-function]

src/geb/package.lisp

@@ -6,7 +6,7 @@
  (defpackage #:geb.main
    (:documentation "Gödel, Escher, Bach categorical model")
    (:use #:common-lisp #:geb.generics #:geb.extension.spec #:serapeum #:geb.mixins #:geb.utils #:geb.spec)
-   (:local-nicknames (#:poly #:geb.poly.spec) (#:bitc #:geb.bitc.spec))
+   (:local-nicknames (#:poly #:geb.poly.spec) (#:bitc #:geb.bitc.spec) (#:seqn #:geb.seqn.spec))
    (:shadowing-import-from #:geb.spec :left :right :prod :case)
    (:export :prod :case :mcar :mcadr :mcaddr :mcdr :name :func :obj :dom :codom)))
 
@@ -21,8 +21,11 @@
   (commutes          pax:function)
   (commutes-left     pax:function)
   (!->               pax:function)
-  (so-eval           pax:function)
-  (so-hom-obj        pax:function)
+  (so-eval           (pax:method () (<natobj> t)))
+  (so-eval           (pax:method () (<substobj> t)))
+  (so-hom-obj        (pax:method () (<natobj> t)))
+  (so-hom-obj        (pax:method () (<substobj> t)))
+  (so-hom-obj        (pax:generic-function))
   (so-card-alg       pax:generic-function)
   (so-card-alg       (pax:method () (<substobj>)))
   (curry             pax:function)
@@ -32,7 +35,8 @@
   (text-name         pax:generic-function)
 
   "These utilities are ontop of [CAT-OBJ]"
-  (maybe             (pax:method () (<substobj>))))
+  (maybe             (pax:method () (<substobj>)))
+  (maybe             (pax:method () (<natobj>))))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Standard Library throughout the codebase
@@ -54,8 +58,8 @@
  (defpackage #:geb.trans
    (:documentation "Gödel, Escher, Bach categorical model")
    (:use #:common-lisp #:serapeum #:geb.mixins #:geb.utils #:geb.spec #:geb.main
-         #:geb.generics)
-   (:local-nicknames (#:poly #:geb.poly.spec) (#:bitc #:geb.bitc.spec))
+         #:geb.generics #:geb.seqn.spec #:geb.seqn.main)
+   (:local-nicknames (#:poly #:geb.poly.spec) (#:bitc #:geb.bitc.spec) (#:seqn #:geb.seqn.spec))
    (:shadowing-import-from #:geb.spec :left :right :prod :case)
    (:export :prod :case :mcar :mcadr :mcaddr :mcdr :name :func :obj)))
 
@@ -67,7 +71,26 @@ into other categorical data structures."
   (to-poly    (pax:method () (<substobj>)))
   (to-poly    (pax:method () (<substmorph>)))
   (to-circuit (pax:method () (<substmorph> t)))
-  (to-bitc    (pax:method () (<substmorph>))))
+  (to-bitc    (pax:method () (<substmorph>)))
+  (to-seqn    (pax:method () (<substobj>)))
+  (to-seqn    (pax:method () (geb.extension.spec:<natobj>)))
+  (to-seqn    (pax:method () (comp)))
+  (to-seqn    (pax:method () (init)))
+  (to-seqn    (pax:method () (terminal)))
+  (to-seqn    (pax:method () (inject-left)))
+  (to-seqn    (pax:method () (inject-right)))
+  (to-seqn    (pax:method () (case)))
+  (to-seqn    (pax:method () (project-left)))
+  (to-seqn    (pax:method () (project-right)))
+  (to-seqn    (pax:method () (pair)))
+  (to-seqn    (pax:method () (distribute)))
+  (to-seqn    (pax:method () (geb.extension.spec:nat-div)))
+  (to-seqn    (pax:method () (geb.extension.spec:nat-const)))
+  (to-seqn    (pax:method () (geb.extension.spec:nat-inj)))
+  (to-seqn    (pax:method () (geb.extension.spec:one-bit-to-bool)))
+  (to-seqn    (pax:method () (geb.extension.spec:nat-decompose)))
+  (to-seqn    (pax:method () (geb.extension.spec:nat-eq)))
+  (to-seqn    (pax:method () (geb.extension.spec:nat-lt))))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;; bool module
@@ -180,7 +203,7 @@ The functions given work on this."
   (gapply                     (pax:method () (opaque t)))
   (geb-bool::@geb-bool        pax:section)
   (geb-list::@geb-list        pax:section)
-  (geb.trans:@geb-translation pax:section)
+  (geb.trans::@geb-translation pax:section)
   (@geb-utility               pax:section))
 
 (pax:defsection @geb-examples (:title "Examples")