On Tue, Dec 25, 2012 at 10:41 PM, Ian Johnson
<blindbravado@gmail.com> wrote:
I see no one's answered; I'm not sure if no one's interested, or if this is just over everyone's head. Accordingly, the following is the same idea in a different context, one that I know at least a few jbopre are familiar with. But if you don't know any Haskell, this post isn't going to do you any good.
The example I have in mind comes from the use of monads in Haskell, and specifically it has to do with how we think about do notation. Without do notation, we get things like this:
m1 >>= \x1 -> m2 >>= \x2 -> f x1 x2
As a concrete example:
getLine >>= \str1 -> getLine >>= \str2 -> putStrLn $ str1 ++ str2
is an IO action that gets two strings from the user and prints their concatenation.
As is, this is normal; variables which are arguments to the second argument to >>= are lambda variables, with corresponding scope. str1 and str2 don't "exist" in the natural mental model of this code, they're just names of the arguments that tell the code how to use the results of the two getLine actions. You could imagine "\str1 -> getLine ..." being a black box function with a name, that you attach to getLine, and then str1 and str2 vanish entirely.
As we know, though, this model gets cumbersome when we start bringing together a lot of monadic values into the same value using >>=, so there's do notation to make things less troubling. The above looks like
do str1 <- getLine
str2 <- getLine
putStrLn $ str1 ++ str2
in do notation. While this notation desugars to the above, the way that we model it mentally is different. Because the functions are hidden and the binds to lambdas are written analogously to assignments, we think of str1 and str2 as values unto themselves. They are instantiated in our mental model of the code. Most of the time, this model is fine, and indeed more useful than the model above, even though it is rather different from what actually is going on. The cases when this model works poorly (such as the reverse state monad that some of you may have seen) seem completely bizarre when written in do notation, because you can't think of those cases as basically operating like an imperative DSL.
This instantiation, like the instantiation of quantified variables that I mentioned previously, doesn't actually make logical sense, but is a model that makes it easier to reason about the code without having to deal with functions as extensively as we would otherwise. And yet...it's sort of troubling that we think like this, because we really can't do this while preserving everything about the desugared code. It'd be really nice to be able to do such a thing (things like {da goi ko'a} essentially, like in the original post) in Lojban, but I'm really not sure whether it should be allowed, since it really is an interaction with logic that isn't actually logical at all.
As before, I'm open to thoughts, although I admit that this prompt isn't particularly specific.
mu'o mi'e la latro'a
On Mon, Dec 24, 2012 at 6:53 PM, Ian Johnson
<blindbravado@gmail.com> wrote:
This is rather subtle, so I think it's best to begin with an example. This example isn't all that mathematically heavy, but it does involve the interaction of several sentences which each have a "forall exists forall" quantifier structure. This does have something to do with Lojban, but it will be a while before that is actually clear. You've been warned :)
Suppose g : R->R is uniformly continuous and f : R -> R is integrable on [a,b]. Define the new function
(f * g)(x) = integral from a to b of g(x-z) f(z) dz
We want to show that the function f * g is continuous at every point, that is:
(for all x in R,e1 > 0)(there exists d1 > 0)(for all y in R) |x-y| < d1 -> |(f * g)(x) - (f * g)(y)| < e1.
(I write quantifiers in almost-prenex-normal form; my apologies if it is hard to read.)
Let e1 > 0.
Using the uniform continuity of g we have
(for all e2 > 0)(exists d2 > 0)(for all x,y in R) |x-y| < d2 -> |g(x) - g(y)| < e2.
So let e2 > 0, obtain the desired d2 > 0, and take x,y with |x-y| < d2. Then:
| (f * g)(x) - (f * g)(y) | = | integral from a to b of f(z) (g(x-z) - g(y-z)) dz |
<= integral from a to b of |f(z) (g(x-z) - g(y-z))| dz
= integral from a to b of |f(z)| |g(x-z) - g(y-z)| dz
< integral from a to b of |f(z)| e2 dz
= Me2
where M = integral from a to b of |f(z)| exists and is finite by assumption.
(Now comes the weird part.)
Setting e2 = e1/M, obtain d2 using the continuity of g, then set d1=d2. Then if |x-y| < d1, from the above |(f * g)(x) - (f * g)(y)| < M e1/M = e1 as desired. Thus f*g is continuous at every point.
What is weird here is that we're playing with e2 and d2 as if they're real. e1 and d1 are interacted with as the quantifier structure suggests: you introduce e1, do some work, and find a valid value of d1. But e2 is now instantiated (in this case in a trivial way, thankfully) under the e1 quantifier, and then d2 is instantiated under the e2 quantifier, followed by folding back up to obtain the original statement. None of this instantiation is "real", it's all syntactic, but we operate better when objects appear to be concrete. This is all ultimately valid reasoning, and indeed can be compressed so that everything is in normal form, but syntactically it's very strange, because it's analogous to {da goi ko'a}, which as I think most of us know doesn't actually make any sense.
I was originally curious about this because I don't know how I would render proofs like this in Lojban; I would be forced, in order to "set d1=d2" and such, to bind d2, which is bound under a quantifier, to a variable, which doesn't actually make logical sense.
Any thoughts?
mu'o mi'e la latro'a