Since Waldek is reviewing Product domain I thought this might be the time to
raise another question.
I would like to model the equivalence between logic and Cartesian closed
categories.
What I would like to do is something like this (where A,B are different
types):
(1) -> conjunction(a:A,b:B)
(1) a and b
Type: PropositionalFormula Product(A,B)
An similarly for disjunction and implies:
(1) -> disjunction(a:A,b:B)
(1) a or b
Type: PropositionalFormula Sum(A,B)
(1) -> implies(a:A,b:B)
(1) a -> b
Type: PropositionalFormula Exponent(A,B)
Of course this does not work at present, what happens is this:
(1) -> PROPA := PropositionalFormula NonNegativeInteger
(1) PropositionalFormula NonNegativeInteger
Type: Domain
(2) -> pa:PROPA := 1
(2) 1
Type: PropositionalFormula NonNegativeInteger
(3) -> PROPB := PropositionalFormula PI
(3) PropositionalFormula PositiveInteger
Type: Domain
(4) -> pb:PROPB := 2
(4) 2
Type: PropositionalFormula PositiveInteger
(5) -> PROPC := PropositionalFormula Symbol
(5) PropositionalFormula Symbol
Type: Domain
(6) -> pc:PROPC := 'c
(6) c
Type: PropositionalFormula Symbol
(7) -> conjunction(pa,pb)
(7) 1 and 2
Type: PropositionalFormula NonNegativeInteger
(8) -> conjunction(pa,pc)
There are 1 exposed and 0 unexposed library operations named
conjunction having 2 argument(s) but none was determined to be
applicable.
It seems to me that it would be easy to define Product,Sum and Exponent, as
required above, as domains which extend SetCategory and are represented by
Record(A,B), Union(A,B) and A-> B respectively.
However this would not be compatible with existing PropositionalFormula and it
would not be closed. That is I would like:
PropositionalFormula Product(A,B)
PropositionalFormula Sum(A,B)
PropositionalFormula Exponent(A,B)
all to be treated as: PropositionalFormula SetCategory
Can that be done in a way that is compatible with SPAD static typing.
Martin
------------------------------------------------------------------------------
The demand for IT networking professionals continues to grow, and the
demand for specialized networking skills is growing even more rapidly.
Take a complimentary Learning@Cisco Self-Assessment and learn
about Cisco certifications, training, and career opportunities.
http://p.sf.net/sfu/cisco-dev2dev
_______________________________________________
open-axiom-devel mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
