diff --git a/src/geb/package.lisp b/src/geb/package.lisp index 832cf8bda..d1a5ceb53 100644 --- a/src/geb/package.lisp +++ b/src/geb/package.lisp @@ -25,7 +25,6 @@ (so-eval (pax:method () ( t))) (so-hom-obj (pax:method () ( t))) (so-hom-obj (pax:method () ( t))) - (so-hom-obj (pax:generic-function)) (so-card-alg pax:generic-function) (so-card-alg (pax:method () ())) (curry pax:function) diff --git a/src/generics/generics.lisp b/src/generics/generics.lisp index 906584b63..0775c28b2 100644 --- a/src/generics/generics.lisp +++ b/src/generics/generics.lisp @@ -40,10 +40,10 @@ to the codomain of MCADR")) case is simply wrapping the term in a [coprod][geb.spec:coprod] of [so1][geb.spec:so1]")) -(defgeneric so-eval (object1 object2) +(defgeneric so-hom-obj (object1 object2) (:documentation - "Takes in X and Y Geb objects and provides an evaluation morphism -(prod (so-hom-obj X Y) X) -> Y")) + "Takes in X and Y Geb objects and provides an internal hom-object +(so-hom-obj X Y) representing a set of functions from X to Y")) (defgeneric so-eval (object1 object2) (:documentation diff --git a/src/generics/package.lisp b/src/generics/package.lisp index f8838bd5f..3e18e5596 100644 --- a/src/generics/package.lisp +++ b/src/generics/package.lisp @@ -15,6 +15,7 @@ examples often given in the specific methods" (gapply pax:generic-function) (well-defp-cat pax:generic-function) (maybe pax:generic-function) + (so-hom-obj pax:generic-function) (so-eval pax:generic-function) (to-circuit pax:generic-function) (to-bitc pax:generic-function) diff --git a/src/lambda/lambda.lisp b/src/lambda/lambda.lisp index c054159d0..575e9b7f6 100644 --- a/src/lambda/lambda.lisp +++ b/src/lambda/lambda.lisp @@ -8,11 +8,11 @@ :accessor mcadr :documentation "")) (:documentation - "Stand-in for the [SO-HOM-OBJ][GEB.MAIN:SO-HOM-OBJ] object. It does not have + "Stand-in for the [SO-HOM-OBJ][GEB.COMMON:SO-HOM-OBJ] object. It does not have any computational properties and can be seen as just a function of two arguments with accessors [MCAR][generic-function] to the first argument and [MCADR][generic-function] to the second argument. There is an evident canonical -way to associate [FUN-TYPE][class] and [SO-HOM-OBJ][GEB.MAIN:SO-HOM-OBJ] +way to associate [FUN-TYPE][class] and [SO-HOM-OBJ][GEB.COMMON:SO-HOM-OBJ] pointwise.")) (defun fun-type (mcar mcadr) @@ -88,7 +88,7 @@ from the left starting with 0." (defgeneric ann-term1 (ctx tterm) (:documentation "Given a list of [SUBSTOBJ][GEB.SPEC:SUBSTOBJ] objects with -[SO-HOM-OBJ][GEB.MAIN:SO-HOM-OBJ] occurences replaced by [FUN-TYPE][class] +[SO-HOM-OBJ][GEB.COMMON:SO-HOM-OBJ] occurences replaced by [FUN-TYPE][class] and an [STLC][type] similarly replacing type occurences of the hom object to [FUN-TYPE][class], provides the [TTYPE][generic-function] accessor to all subterms as well as the term itself, using [FUN-TYPE][class]. Once again, @@ -202,7 +202,7 @@ the context on the left as well. For more info check [LAMB][class]")) (defun fun-to-hom (t1) "Given a [SUBSTOBJ][GEB.SPEC:SUBSTOBJ] whose subobjects might have a [FUN-TYPE][class] occurence replaces all occurences of [FUN-TYPE][class] with a -suitable [SO-HOM-OBJ][GEB.MAIN:SO-HOM-OBJ], hence giving a pure +suitable [SO-HOM-OBJ][GEB.COMMON:SO-HOM-OBJ], hence giving a pure [SUBSTOBJ][GEB.SPEC:SUBSTOBJ] ```lisp @@ -266,9 +266,9 @@ occurences - re-annotates the term and its subterms with actual (defun annotated-term (ctx term) "Given a context consisting of a list of [SUBSTOBJ][GEB.SPEC:SUBSTOBJ] -with occurences of [SO-HOM-OBJ][GEB.MAIN:SO-HOM-OBJ] replaced by +with occurences of [SO-HOM-OBJ][GEB.COMMON:SO-HOM-OBJ] replaced by [FUN-TYPE][class] and an [STLC][type] term with similarly replaced occurences -of [SO-HOM-OBJ][GEB.MAIN:SO-HOM-OBJ], provides an [STLC][type] with all +of [SO-HOM-OBJ][GEB.COMMON:SO-HOM-OBJ], provides an [STLC][type] with all subterms typed, i.e. providing the [TTYPE][generic-function] accessor, which is a pure [SUBSTOBJ][GEB.SPEC:SUBSTOBJ]" (ann-term2 (ann-term1 ctx term))) @@ -279,19 +279,19 @@ which is a pure [SUBSTOBJ][GEB.SPEC:SUBSTOBJ]" (defun type-of-term-w-fun (ctx tterm) "Given a context consisting of a list of [SUBSTOBJ][GEB.SPEC:SUBSTOBJ] with -occurences of [SO-HOM-OBJ][GEB.MAIN:SO-HOM-OBJ] replaced by [FUN-TYPE][class] +occurences of [SO-HOM-OBJ][GEB.COMMON:SO-HOM-OBJ] replaced by [FUN-TYPE][class] and an [STLC][type] term with similarly replaced occurences of -[SO-HOM-OBJ][GEB.MAIN:SO-HOM-OBJ], gives out a type of the whole term with -occurences of [SO-HOM-OBJ][GEB.MAIN:SO-HOM-OBJ] replaced by [FUN-TYPE][class]." +[SO-HOM-OBJ][GEB.COMMON:SO-HOM-OBJ], gives out a type of the whole term with +occurences of [SO-HOM-OBJ][GEB.COMMON:SO-HOM-OBJ] replaced by [FUN-TYPE][class]." (ttype (ann-term1 ctx tterm))) ;; Actual type info (defun type-of-term (ctx tterm) "Given a context consisting of a list of [SUBSTOBJ][GEB.SPEC:SUBSTOBJ] with -occurences of [SO-HOM-OBJ][GEB.MAIN:SO-HOM-OBJ] replaced by [FUN-TYPE][class] +occurences of [SO-HOM-OBJ][GEB.COMMON:SO-HOM-OBJ] replaced by [FUN-TYPE][class] and an [STLC][type] term with similarly replaced occurences of -[SO-HOM-OBJ][GEB.MAIN:SO-HOM-OBJ], provides the type of the whole term, +[SO-HOM-OBJ][GEB.COMMON:SO-HOM-OBJ], provides the type of the whole term, which is a pure [SUBSTOBJ][type]." (fun-to-hom (type-of-term-w-fun ctx tterm))) @@ -300,9 +300,9 @@ which is a pure [SUBSTOBJ][type]." (defgeneric well-defp (ctx tterm) (:documentation "Given a context consisting of a list of [SUBSTOBJ][GEB.SPEC:SUBSTOBJ] -with occurences of [SO-HOM-OBJ][GEB.MAIN:SO-HOM-OBJ] replaced by +with occurences of [SO-HOM-OBJ][GEB.COMMON:SO-HOM-OBJ] replaced by [FUN-TYPE][class] and an [STLC][type] term with similarly replaced -occurences of [SO-HOM-OBJ][GEB.MAIN:SO-HOM-OBJ], checks that the term +occurences of [SO-HOM-OBJ][GEB.COMMON:SO-HOM-OBJ], checks that the term is well-defined in the context based on structural rules of simply typed lambda calculus. returns the t if it is, otherwise returning nil")) diff --git a/src/lambda/trans.lisp b/src/lambda/trans.lisp index 7bc48f2cf..ae5d94293 100644 --- a/src/lambda/trans.lisp +++ b/src/lambda/trans.lisp @@ -91,11 +91,11 @@ morphism of the GEB category using a Maybe monad wrapper, that is, given a context G and a term t of type A produces a morphism with domain (stlc-ctx-maybe context) and codomain (maybe A). -Terms come from [STLC][type] with occurences of [SO-HOM-OBJ][GEB.MAIN:SO-HOM-OBJ] +Terms come from [STLC][type] with occurences of [SO-HOM-OBJ][GEB.COMMON:SO-HOM-OBJ] replaced by [FUN-TYPE][class] and should come without the slow of [TTYPE][generic-function] accessor filled for any of the subterms. Context should be a list of [SUBSTOBJ][GEB.SPEC:SUBSTOBJ] with the caveat that instead of -[SO-HOM-OBJ][GEB.MAIN:SO-HOM-OBJ] we ought to use [FUN-TYPE][class], a stand-in +[SO-HOM-OBJ][GEB.COMMON:SO-HOM-OBJ] we ought to use [FUN-TYPE][class], a stand-in for the internal hom object with explicit accessors to the domain and the codomain. 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 @@ -283,10 +283,10 @@ This follows from the fact that bool arapped in maybe is 1 + (bool + bool)" "Compiles a checked term in an appropriate context into the morphism of the GEB category. In detail, it takes a context and a term with following restrictions: Terms come from [STLC][type] with occurences of -[SO-HOM-OBJ][GEB.MAIN:SO-HOM-OBJ] replaced by [FUN-TYPE][class] and should +[SO-HOM-OBJ][GEB.COMMON:SO-HOM-OBJ] replaced by [FUN-TYPE][class] and should come without the slow of [TTYPE][generic-function] accessor filled for any of the subterms. Context should be a list of [SUBSTOBJ][GEB.SPEC:SUBSTOBJ] with -the caveat that instead of [SO-HOM-OBJ][GEB.MAIN:SO-HOM-OBJ] we ought to use +the caveat that instead of [SO-HOM-OBJ][GEB.COMMON:SO-HOM-OBJ] we ought to use [FUN-TYPE][class], a stand-in for the internal hom object with explicit accessors to the domain and the codomain. Once again, note that it is important for the context and term to be giving as per above description. While not @@ -484,7 +484,7 @@ and iteratively applies Maybe to its elements." (-> so-hom (substobj substobj) (or t substobj)) (defun so-hom (dom cod) "Computes the hom-object of two [SUBSTMORPH]s" - (geb:so-hom-obj dom cod)) + (so-hom-obj dom cod)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Utility Functions