Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Move so-hom-obj Generic #152

Merged
merged 1 commit into from
Oct 11, 2023
Merged

Move so-hom-obj Generic #152

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 0 additions & 1 deletion src/geb/package.lisp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,6 @@
(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)
Expand Down
6 changes: 3 additions & 3 deletions src/generics/generics.lisp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
1 change: 1 addition & 0 deletions src/generics/package.lisp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
26 changes: 13 additions & 13 deletions src/lambda/lambda.lisp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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,
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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)))
Expand All @@ -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)))

Expand All @@ -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"))
Expand Down
10 changes: 5 additions & 5 deletions src/lambda/trans.lisp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
Loading