Martin Baker <ax87...@martinb.com> writes: | 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.
OK. One thing to realize is that the equivalence is through an *interpretation* of logical formulae. So, you would like to setup an interpretation package with appropriate entry point to compute the interpretation. | | 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) this is just *one* (valid) interpretation, and there other equally valid interpretation, so you probably don't it to be the only interpretation in the system. For me that implies that we would have strong reasons to make it the default interpretation -- which would require serious modification of either PropositionalFormula or the intrepreter or both. | 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. Almost all operations in PropositionalLogic are homogeneous, that means that the interpreter has to find a common type for the arguments when they are of differing types (like pa and pc). When that cannot be done, you get an error. | 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. Agreed. | | 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. SetCategory is a category, not a domain, so is not appropriate argument for PropositionalFormula. Categories cannot be constructor arguments -- all AXIOM flavours affected. In OpenAxiom, you use the domain Domain, so you would get something like PropositionalFormula Domain which is probably what you want. -- Gaby ------------------------------------------------------------------------------ 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 open-axiom-devel@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
