Message-Id: <199412100323.AA14654@nfs1.digex.net>
Date:         Sat, 10 Dec 1994 01:02:46 GMT
Reply-To: ia@stryx.demon.co.uk
Sender: Lojban list <LOJBAN@CUVMB.BITNET>
From: Iain Alexander <ia@STRYX.DEMON.CO.UK>
Subject:      Re: TECH:  existential quantification
To: Bob LeChevalier <lojbab@access.digex.net>
Status: RO

la xorxes. cusku di'e sa'ecu'i
> What you describe (which I've deleted) is what I understand as the
> difference between transparent and opaque reference.  I would refer to
> those two as (lo nu mi limna) and (lo'e nu mi limna).

Yes, exactly, as far as it goes.

I'm assuming that we agree that opacity arises because there's
a subordinate predication, which is elided in idiomatic English
and a large number of other languages.
The problem is that we start with {mi djica tu'a lo plise},
which becomes {mi djica tu'a lo nu co'e lo plise},
...
which becomes {mi djica tu'a lo nu co'e lo nu co'e lo nu co'e lo plise},
...

Each time we clarify the opacity by supplying the previously
elided predication, we find an opaque reference to an event,
which gives us the same problem all over again.  We need a way
of short-circuiting this.  I was suggesting {za'i} as the abstraction,
but this turns out to have been a misunderstanding.  You are suggesting
{lo'e} as the gadri, which I have considered myself in the past,
and this may turn out to be the best answer.  But I still have
misgivings about {lo'e} as the solution to this problem,
at least partly because I'm not sure why it works, because I've
no idea how I would translate it into Predicate Calculus.
It's a sort of magic wand that intuitively seems to give the
right semantics.

Combinatory Logic is essentially an alternative
formulation of the ideas of Lambda Calculus, and that has
something called the Y combinator (which can be translated
into Lambda Calculus), which is a sort of magic wand
which allows you to define functions recursively.
That's OK, because there is a formal definition for the
Y combinator, and you can work through the way it operates,
and get some kind of understanding of how it works,
and then forget about the details and just use it.

Our problem here appears to be one of expressing something
in Predicate Calculus (or at least, our implementation
of an extended Predicate Calculus), and I would be a lot
happier if we had a solution which could be described
in those terms.

If there _was_ an abstraction that meant what I was suggesting
{za'i} meant, I'd admittedly still not got a precise
Predicate Calculus definition for it, but I thought I could
see vaguely what it might look like, more than I currently
can with {lo'e}.

mu'o mi'e .i,n.
--
Iain Alexander (ia@stryx.demon.co.uk)