On Sun, Feb 11, 2001 at 09:17:53PM -0800, William Lee Irwin III wrote:
mod an ideal generated by a polynomial, e.g. 1/(1-x) mod (1+x^2).
On Mon, Feb 12, 2001 at 01:23:53PM -0500, Dylan Thurston wrote:
Sorry, isn't (1+x^2) invertible in Z[[x]]?
You've caught me asleep at the wheel again. Try 1/(1-x) mod 2+x^2. Then x^(2n) -> (-2)^n x^(2n+1) -> (-2)^n x so our process isn't finite again, and as 2 is not a unit in Z, 2+x^2 is not a unit in Z[[x]]. On Sun, Feb 11, 2001 at 09:17:53PM -0800, William Lee Irwin III wrote:
I think it's nice to have the Cauchy principal value versions of things floating around. I know at least that I've had call for using the CPV of exponentiation (and it's not hard to contrive an implementation), but I'm almost definitely an atypical user. (Note, (**) does this today.)
On Mon, Feb 12, 2001 at 01:23:53PM -0500, Dylan Thurston wrote:
Does Cauchy Principal Value have a specific definition I should know? The Haskell report refers to the APL language report; do you mean that definition?
The Cauchy principal value of an integral seems fairly common in complex analysis, and so what I mean by the CPV of exponentiation is using the principal value of the logarithm in the definition w^z = exp (z * log w). Essentially, given an integral from one point to another in the complex plane (where the points can be e^(i*\gamma)*\infty) the Cauchy principal value specifies precisely which contour to use, for if the function has a singularity, connecting the endpoints by a countour that loops about those singularities a number of times will affect the value of the integral. This is fairly standard complex analysis, are you sure you can't dig it up somewhere? It basically says to connect the endpoints of integration by a straight line unless singularities occur along that line, and in that case, to shrink a semicircle about the singularities, and the limit is the Cauchy principal value. More precise definitions are lengthier. On Mon, Feb 12, 2001 at 01:23:53PM -0500, Dylan Thurston wrote:
I'm still agnostic on the Poset issue, but as an aside, let me mention that "Maybe Bool" works very well as a trinary logical type. "liftM2 &&" does the correct trinary and, for instance.
I can only argue against this on aesthetic grounds. (<=) and cousins are not usually typed so as to return Maybe Bool. On Mon, Feb 12, 2001 at 01:23:53PM -0500, Dylan Thurston wrote:
It may be logically prior, but computationally it's not... Note that the axioms for lattices can be stated either in terms of the partial ordering, or in terms of meet and join.
I was under the impression the distinction between lattices and partial orders was the existence of the meet and join operations. Actually, I think my argument centers about the use of the antisymmetry of the relation (<=) being used to define computational equality in some instances. Can I think of any good examples? Well, a contrived one would be that on types, if there is a substitution S such that S t = t' (structurally), where we might say that t' <= t, and also a substitution S' so such that S' t' = t (again, structurally) where we might say that t <= t', so we have then t == t' (semantically). Yes, I realize this is not a great way to go about this. Another (perhaps contrived) example would be ordering expression trees by the flat CPO bottom <= _ on constants of a signature, and the natural business where if the trees differ in structure, they're incomparable, except where bottom would be compared with something non-bottom, in which case (<=) holds. In this case, we might want equality to be that two expression trees t, t' are equal iff there are sequences of reductions r, r' such that r t = r' t' (again, structurally). You might argue that the notion of structural equality underlying these is some sort of grounds for the dependency, and I think that hits on the gray area where design decisions come in. What I'm hoping the examples demonstrate is the mathematical equality and ordering (in some metalanguage) underlie both of the computational notions, and that the computational notions may very reverse or break the dependency class Eq t => Ord t where ... especially when the structure of the data does not reflect the equivalence relation we'd like (==) to denote. Cheers, Bill