What binary operation lambda quantifier corresponds to?

["Followup-To:" nach comp.lang.functional gesetzt.]
Tegiri Nenashi <TegiriNenashi@gmail.com> schrieb:
> Observation: all quantuifiers correspond to some binary algebraic
> operation. Consider:
>
> 1. Sigma summation and integral are iterative forms of binary plus.
> 2. Pi-capital product is iterative form of multiplication.
> 3. Lattice supremum is iterative form binary meet.
> 5. Lattice infinum is iterative form binary join.
> 6. Existential and universal quatifiers are lattice supremum and
> infinum.

Dirk Thierbach has already pinted out that this is only true when
you iterate over finite sets. But we're in computer sciences, where
everything is nice and finite

> Now, there must be a binary operation that lambda is iterative form as
> well?

I only see a far-fetched analogy: You can transform a n-ary function
into a unary function by the repeated application of uncurry.

f :: Int -> Int -> Int -> Int -> Int
f = \ a b c d -> a+b+c+d

then becomes

f' :: (((Int, Int), Int), Int) -> Int
f' = (uncurry . uncurry . uncurry) f

Dnia 06-09-2008 o 20:52:22 Tegiri Nenashi <TegiriNenashi@gmail.com>
napisa³(a):

> Now, there must be a binary operation that lambda is iterative form as
> well?

You may think of the lambda operator as of a kind of product - namely:

a) a type \lambda X:U . T[X] corresponds to the prouct \Pi_{X \in U} T[X],

b) a term \lambda x . F[x] corresponds to the product (we need to form
singletons in case F[x] do not admit internal products) \Pi_x {F[x]},
where x varies over its type.


--
Micha³ Przyby³ek

On Sep 7, 3:48 am, Florian Kreidler <m...@privacy.net> wrote:

> Tegiri Nenashi <TegiriNena...@gmail.com> schrieb:

> > Now, there must be a binary operation that lambda is iterative form as
> > well?
>
> I only see a far-fetched analogy: You can transform a n-ary function
> into a unary function by the repeated application of uncurry.
>
> f :: Int -> Int -> Int -> Int -> Int
> f = \ a b c d -> a+b+c+d
>
> then becomes
>
> f' :: (((Int, Int), Int), Int) -> Int
> f' = (uncurry . uncurry . uncurry) f

the maps between products and application
giving the classic hom(X, Z^Y) iso= hom(X x Y, Z)
in the curry/uncurry operations
is precisely the point of my suggesting exponentiation

http://en.wikipedia.org/wiki/Exponential_object

-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-
galathaea: prankster, fablist, magician, liar

On 6 Sep, 19:52, Tegiri Nenashi <TegiriNena...@gmail.com> wrote:
> Observation: all quantuifiers correspond to some binary algebraic
> operation. Consider:
>
> 1. Sigma summation and integral are iterative forms of binary plus.
> 2. Pi-capital product is iterative form of multiplication.
> 3. Lattice supremum is iterative form binary meet.
> 5. Lattice infinum is iterative form binary join.
> 6. Existential and universal quatifiers are lattice supremum and
> infinum.
>
> Now, there must be a binary operation that lambda is iterative form as
> well?

This might have some relevance.

How to Build a Quantifier Machine

http://www.lambdassociates.org/studies/study04.htm

Mark

On Sep 6, 11:50*pm, Dirk Thierbach <dthierb...@usenet.arcornews.de>
wrote:
> Tegiri Nenashi <TegiriNena...@gmail.com> wrote:
> > Observation: all quantuifiers correspond to some binary algebraic
> > operation. Consider:
>
> Or more precisely: Four commonly known "big operations" ...
> ... But these are not "all quantifiers" in the sense of "all 'big' operations".
> > 1. Sigma summation and integral are iterative forms of binary plus.
>
> The integral is more complicated, because it involves (among other
> things) a limit. Also, the integral without bounds behaves a bit
> differently (doesn't reduce to a single value).

Hmm, limit is also quantifier (or "big operation" as you call it -- I
didn't quite follow your objection to the term "quantifier"). In case
of [Riemann] intergral the limit is essentally upper lower bound on
totally ordered set. Therefore, we have two levels of quantification
(with some division in the middle).

Integral without bounds is essentially integral on the segment with
variable upper bound, so there doesn't seem to be anything interesting
here. Or, considering your next question maybe there is...

> And what about differentiation? It's the inverse operation of
> integration, so what binary operation should it correspond to? :-)

Derivative is the limit, so what is the problem? However, considering
that definite integral has two levels of "quantification" and
indefinte integral is even more complex expression, the skewed
symmetry is interesting indeed.

The rest of your message is little too advanced for me to comment on.
I have one more quesion, though. In "introduction to mathematical
logic" p.31 Church wrote several lambda expressions like this

lambda x ( x > 0 )

How can lambda abstraction be applied to a predicate?

On Sep 8, 9:49*am, Tegiri Nenashi <TegiriNena...@gmail.com> wrote:
> Hmm, limit is also quantifier (or "big operation" as you call it -- I
> didn't quite follow your objection to the term "quantifier").

Limit is also quantifier, but I have trouble finding an associate
binary operation! (My mistake was focusing on monothonic sequences
only).

On Sep 8, 10:02*am, Tegiri Nenashi <TegiriNena...@gmail.com> wrote:
> On Sep 8, 9:49*am, Tegiri Nenashi <TegiriNena...@gmail.com> wrote:
>
> > Hmm, limit is also quantifier (or "big operation" as you call it -- I
> > didn't quite follow your objection to the term "quantifier").
>
> Limit is also quantifier, but I have trouble finding an associate
> binary operation! (My mistake was focusing on monothonic sequences
> only).

Writing in small increments, sorry. Limit seems to corresond to the
following associative noncommutative operation:

(x,y) -> y

which is informally "take the second element".

[Reduced followup to clf]

Tegiri Nenashi <TegiriNenashi@gmail.com> wrote:
> On Sep 6, 11:50*pm, Dirk Thierbach <dthierb...@usenet.arcornews.de>
> wrote:
>> Tegiri Nenashi <TegiriNena...@gmail.com> wrote:
>> > Observation: all quantuifiers correspond to some binary algebraic
>> > operation. Consider:

>> Or more precisely: Four commonly known "big operations" ...
>> ... But these are not "all quantifiers" in the sense of "all 'big'
>> operations".

>> > 1. Sigma summation and integral are iterative forms of binary plus.

>> The integral is more complicated, because it involves (among other
>> things) a limit. Also, the integral without bounds behaves a bit
>> differently (doesn't reduce to a single value).

> Hmm, limit is also quantifier (or "big operation" as you call it -- I
> didn't quite follow your objection to the term "quantifier").

Like the english term "quantity", "quantifier" comes from the latin
word "quantus" which means something like "how much?". So in the strict
(or original) sense, a quantifier tells you something about how many
things are involved. So really only "exists" (at least one thing),
"forall" (all things), and others like "exactly one" (often written
like "exists" with an additional exclamation mark) should be called
"quantifiers".

I'm not exactly sure what the english term for sigma, pi etc. is. In the
TeX-book, Knuth calls them "big operators", so I did the same.

> In case of [Riemann] intergral the limit is essentally upper lower
> bound on totally ordered set. Therefore, we have two levels of
> quantification (with some division in the middle).

And some other stuff, which becomes clearer if you generalize it:
Measures, sigma-algebras, and so on. So there's much more involved than
just a simple sum.

>> And what about differentiation? It's the inverse operation of
>> integration, so what binary operation should it correspond to? :-)

> Derivative is the limit, so what is the problem?

It's not a problem. I just wanted to point out that you already know
examples of other operators, which are not directly related to binary
operations.

> The rest of your message is little too advanced for me to comment on.
> I have one more quesion, though. In "introduction to mathematical
> logic" p.31 Church wrote several lambda expressions like this

> lambda x ( x > 0 )

> How can lambda abstraction be applied to a predicate?

You can apply lambda abstraction to every expression that involves
variables.

Maybe it becomes clearer if we try to look at some examples: Consider a
real valued function f,

f(x) = sin x + cos x.

I could just take the expression on the right hand side and put a lambda
in front. Then this would be a function, so an alternative way to write
the above equation is

f = lambda x. sin x + cos x

In this line, there are now *functions* on both side of the equal sign.

One can view a predicate as a function the returns boolean values.
So I could define a predicate as

p(x) = x > 0

or, in the same way as above, I could just view the whole expression
as a function and write

p = lambda x. x > 0

Does that help?

BTW, in some functional programming languages like e.g. Haskell you can
actually use both ways to define a function.

- Dirk

[Reduced followup to clf]

Tegiri Nenashi <TegiriNenashi@gmail.com> wrote:
> On Sep 8, 10:02*am, Tegiri Nenashi <TegiriNena...@gmail.com> wrote:
>> On Sep 8, 9:49*am, Tegiri Nenashi <TegiriNena...@gmail.com> wrote:

>> Limit is also quantifier, but I have trouble finding an associate
>> binary operation! (My mistake was focusing on monothonic sequences
>> only).

> Writing in small increments, sorry. Limit seems to corresond to the
> following associative noncommutative operation:
>
> (x,y) -> y
>
> which is informally "take the second element".

No, it doesn't :-) Otherwise the limit should always be one of the
arguments. But we know for example that

lim 1/n = 0
n -> oo

where each of the "arguments" 1/n is bigger than zero.

(There are several ways to define limits, the version with epsilons
is maybe the most accessible. I suggest you look it up.)

- Dirk

On Sep 8, 10:24*am, Dirk Thierbach <dthierb...@usenet.arcornews.de>
wrote:
> Tegiri Nenashi <TegiriNena...@gmail.com> wrote:
> > Limit seems to corresond to the
> > following associative noncommutative operation:
>
> > (x,y) -> y
>
> > which is informally "take the second element".
>
> No, it doesn't :-) Otherwise the limit should always be one of the
> arguments.

I don't understand this argument. Let be more specific: we have an
(infinite) list of numbers

x(0), x(1), x(2), ...

and want to evaluate it to a single number. By induction we can
establish that the limit restricted to any finite prefix of this list
equals to the last number in the prefix. How does it follow that for
infinite list the limit has to be equal to one of the numbers on the
list?

> (There are several ways to define limits, the version with epsilons
> is maybe the most accessible. I suggest you look it up.)

Well, if I wonder about big operators expressed in terms of binary
operations, probably the last thing to do is to look up into a
definition that uses quantifiers (that is other big operators)...