Re: [open-axiom-devel] [Axiom-math] Type equivalence of domains in Axiom and Aldor
A system for computer algebra and symbolic mathematics
Brought to you by:
dos-reis
From: Ralf H. <ra...@he...> - 2007-10-28 20:32:10
|
> Def: Two domains P and Q are equivalent if and only if both domains satisfy > exactly the same set of categories: (P has x) = (Q has x) for all Category > expressions x *and* neither P nor Q has any explicit exports that are not > provided by some named category. Let's see... Cat: Category == with { coerce: Integer -> %; coerce: % -> Integer; bar: (%, %) -> %; } P: Cat == add { Rep == Integer; import from Rep coerce(x: Integer): % == per x; coerce(x: %): Integer == rep x; bar(x: %, y: %): % == per(rep x + rep y); } ----------------------------------^ Q: Cat == add { Rep == Integer; import from Rep coerce(x: Integer): % == per x; coerce(x: %): Integer == rep x; bar(x: %, y: %): % == per(rep x - rep y); } ----------------------------------^ You are saying that P and Q are equivalent. Ralf |