On Tue, Dec 25, 2012 at 10:41 PM, Ian Johnso= n <blindbravado@gmail.com> wrote:

I see no one's answered; I'm not sure if no one's interested, o= r if this is just over everyone's head. Accordingly, the following is t= he 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 >>=3D \x1 -> m2 >>= =3D \x2 -> f x1 x2
As a concrete example:
getLine >>=3D \str1 -> getLine >>= =3D \str2 -> putStrLn $ str1 ++ str2
is an IO action that gets two st= rings from the user and prints their concatenation.
As is, this is norma= l; variables which are arguments to the second argument to >>=3D are = lambda variables, with corresponding scope. str1 and str2 don't "e= xist" 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 getL= ine actions. You could imagine "\str1 -> getLine ..." being a = black box function with a name, that you attach to getLine, and then str1 a= nd str2 vanish entirely.

As we know, though, this model gets cumbersome when we start bringing t= ogether a lot of monadic values into the same value using >>=3D, so t= here's do notation to make things less troubling. The above looks like<= br> do str1 <- getLine
=A0 =A0=A0 str2 <- getLine
=A0 =A0=A0 putStr= Ln $ str1 ++ str2
in do notation. While this notation desugars to the a= bove, 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 instanti= ated in our mental model of the code. Most of the time, this model is f= ine, 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 p= oorly (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 thin= k 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 sor= t 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 n= ice to be able to do such a thing (things like {da goi ko'a} essentiall= y, like in the original post) in Lojban, but I'm really not sure whethe= r it should be allowed, since it really is an interaction with logic that i= sn't actually logical at all.

As before, I'm open to thoughts, although I admit that this prompt = isn't particularly specific.

mu'o m= i'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. T= his example isn't all that mathematically heavy, but it does inv= olve the interaction of several sentences which each have a "forall ex= ists forall" quantifier structure. This does have something to = do with Lojban, but it will be a while before that is actually clear. You&#= 39;ve been warned :)

Suppose g : R->R is uniformly continuous and f : R -> R is integr= able on [a,b]. Define the new function
(f * g)(x) =3D integral from a to= b of g(x-z) f(z) dz
We want to show that the function f * g is continuo= us at every point, that is:
(for all x in R,e1 > 0)(there exists d1 > 0)(for all y in R) |x-y| &l= t; 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) | =3D | integral from a to b of f(z) (g(x-z) = - g(y-z)) dz |
<=3D integral from a to b of |f(z) (g(x-z) - g(y-z))| = dz
=3D integral from a to b of |f(z)| |g(x-z) - g(y-z)| dz
< integ= ral from a to b of |f(z)| e2 dz
=3D Me2
where M =3D integral from a to b of |f(z)| exists and is finite = by assumption.

(Now comes the weird part.)

Setting e2 =3D e1/= M, obtain d2 using the continuity of g, then set d1=3Dd2. Then if |x-y| <= ; d1, from the above |(f * g)(x) - (f * g)(y)| < M e1/M =3D e1 as desire= d. Thus f*g is continuous at every point.

What is weird here is that we're playing with e2 and d2 as if they&= #39;re real. e1 and d1 are interacted with as the quantifier structure sugg= ests: 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) unde= r the e1 quantifier, and then d2 is instantiated under the e2 quantifier, f= ollowed by folding back up to obtain the original statement. None of this i= nstantiation is "real", it's all syntactic, but we operate be= tter when objects appear to be concrete. This is all ultimately valid reaso= ning, and indeed can be compressed so that everything is in normal form, bu= t syntactically it's very strange, because it's analogous to {da go= i 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 woul= d render proofs like this in Lojban; I would be forced, in order to "s= et d1=3Dd2" and such, to bind d2, which is bound under a quantifier, t= o a variable, which doesn't actually make logical sense.

Any thoughts?

mu'o mi'e la latro'a