Chung-chieh Shan wrote:
On 2005-01-28T20:16:59+0100, Henning Thielemann wrote:
I can't imagine mathematics with side effects, because there is no order of execution.
To clarify, I'm not saying that mathematics may have side effects, but that the language we use to talk about mathematics may have side effects, even control effects with delimited continuations.
I understand.
But what do you mean with 1/O(n^2) ? O(f) is defined as the set of functions bounded to the upper by f. So 1/O(f) has no meaning at the first glance. I could interpret it as lifting (1/) to (\f x -> 1 / f x) (i.e. lifting from scalar reciprocal to the reciprocal of a function) and then as lifting from a reciprocal of a function to the reciprocal of each function of a set. Do you mean that?
Wait a minute -- would you also say that "1+x" has no meaning at the first glance, because "x" is a variable whereas "1" is an integer, so some lifting is called for?
For me 'x' is a place holder for a value. For the expression '1+x' I conclude by type inference that 'x' must be a variable for a scalar value, since '1' is, too. But the expression '1/O(n^2)' has the scalar value '1' on the left of '/' and a set of functions at the right side. Type inference fails, so my next try is to make the operands compatible in a somehow natural way. Since mathematical notation invokes many implicit conversions, it's sometimes no longer unique or obvious what implicit conversion to use. Many users of O(n^2) seem to consider it as a placeholder for some expression, where the value of the expression is bounded by n^2.
I never heard about shift and reset operators, but they don't seem to be operators in the sense of higher-order functions.
Right; they are control operators in the sense that call/cc is a control operator.
So they seem to be operators that work on expressions rather than values. In this respect they are similar to the lambda operator, aren't they?
But I see people writing f(.) + f(.-t) and they don't tell, whether this means (\x -> f x) + (\x -> f (x-t)) or (\x -> f x + f (x-t)) In this case for most mathematicians this doesn't matter because in the above case (+) is silently lifted to the addition of functions.
Yes, so in my mind an environment monad is in effect (so to speak) here, and the difference between the two meanings you pointed out is the difference between
liftM2 (+) (liftM f ask) (liftM f (liftM2 (-) ask (return t)))
and
(+) (liftM f ask) (liftM f (liftM2 (-) ask (return t)))
(where import Monad and Control.Monad.Reader :).
You use 'ask' twice in the second expression. Does this mean that there may be two different values for 'ask'? If this is the case your second interpretation differs from my second interpretation.
I found that using a notation respecting the functional idea allows very clear terms. So I used Haskell notation above to explain, what common mathematical terms may mean.
But Haskell notation does -not- respect the functional idea. First there's the issue of variables: to respect the functional idea we must program in point-free style.
Hm, you are right, I also use function definitions like (\x -> f x + g x) ... Sure, I know from the theory of partial recursive functions that I can do "everything" with "notationally pure functions", but I don't know if it is convenient.
Second there's the issue of types: to respect the (set-theoretic) functional idea we must abolish polymorphism and annotate our lambda abstractions in Church style. Surely we don't want the meaning of our mathematical formulas to depend on the semantics of System F(-omega)!
Church style, System F(-omega), alpha-conversion, lambda calculus, eta reduction, currying - Where can I find some introduction to them? What about Haskell Curry? What about Bourbaki? - I have heard they worked hard to find a unified notation.