What binary operation lambda quantifier corresponds to?

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?

On Sep 6, 3:52*pm, 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?

No.

-- m

On Sep 6, 11:52 am, 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?

if i understand what you mean by lambda quantifier
(as in the standard form on which eval's work through application
e.g. lambda calculus lambdas
with their well known universal properties)
then i would expect the exponential to be the corresponding operation

in other words
given a objects X and Y
a function f from X to Y is an element of the exponential object

X
f elementOf Y

and the evaluation at an element of X is given by

X
eval: Y x X --> Y

(such that a variety of commutative diagrams obtain)

am i talking about the same lambda here?

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

On Sep 6, 3:31*pm, galathaea <galath...@gmail.com> wrote:
> On Sep 6, 11:52 am, 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?
>
> if i understand what you mean by lambda quantifier
> (as in the standard form on which eval's work through application
> *e.g. lambda calculus lambdas
> * *with their well known universal properties)
> then i would expect the exponential to be the corresponding operation
>
> in other words
> * given a objects X and Y
> a function f from X to Y is an element of the exponential object
>
> * * * * * * * * X
> * f elementOf *Y
>
> and the evaluation at an element of X is given by
>
> * * * * *X
> * eval: Y *x X *--> *Y
>
> (such that a variety of commutative diagrams obtain)
>
> am i talking about the same lambda here?

Church lambda abstraction (lambda calculus should be evident from
comp.lang.functional in the newsgroup list:-)

Exponentiation is unary operation. In binary form -- exp(x,y) --
exponentiation is not associative, that would also disqualify it.

On Sep 6, 6:03 pm, Tegiri Nenashi <TegiriNena...@gmail.com> wrote:
> On Sep 6, 3:31 pm, galathaea <galath...@gmail.com> wrote:
>
>
>
> > On Sep 6, 11:52 am, 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?
>
> > if i understand what you mean by lambda quantifier
> > (as in the standard form on which eval's work through application
> > e.g. lambda calculus lambdas
> > with their well known universal properties)
> > then i would expect the exponential to be the corresponding operation
>
> > in other words
> > given a objects X and Y
> > a function f from X to Y is an element of the exponential object
>
> > X
> > f elementOf Y
>
> > and the evaluation at an element of X is given by
>
> > X
> > eval: Y x X --> Y
>
> > (such that a variety of commutative diagrams obtain)
>
> > am i talking about the same lambda here?
>
> Church lambda abstraction (lambda calculus should be evident from
> comp.lang.functional in the newsgroup list:-)

not at all

comp.lang.functional could be talking about
any of many quantifiers

obviously i guessed right
but with only 21 returned sources
in a quoted google search of the term
(some of which are your post)
you must understand that it is not common

> Exponentiation is unary operation.

i would think
since i explicitly wrote which operation i was discussing
you would know i am not talking about application of e^(.)

you seem to have poor people skills
(fyi)

> In binary form -- exp(x,y) --
> exponentiation is not associative, that would also disqualify it.

why do you think an operation must be associative?

there are logics with nonassociative conjunction
for instance

is conjunction not a binary operation?

you don't seem to have a very clear idea what you want
and you seem to be dismissive and argumentative
so i might not respond any furthur

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

On Sep 6, 6:34*pm, galathaea <galath...@gmail.com> wrote:
> On Sep 6, 6:03 pm, Tegiri Nenashi <TegiriNena...@gmail.com> wrote:
>
> > On Sep 6, 3:31 pm, galathaea <galath...@gmail.com> wrote:
> > > if i understand what you mean by lambda quantifier
> > > (as in the standard form on which eval's work through application
> > > *e.g. lambda calculus lambdas
> > > * *with their well known universal properties)
> > > then i would expect the exponential to be the corresponding operation

> > > in other words
> > > * given a objects X and Y
> > > a function f from X to Y is an element of the exponential object
>
> > > * * * * * * * * X
> > > * f elementOf *Y
>
> > > and the evaluation at an element of X is given by
>
> > > * * * * *X
> > > * eval: Y *x X *--> *Y
>
> > > (such that a variety of commutative diagrams obtain)

Could you please be more specific what algebraic structure you have in
mind? Specifically, what are the elements ("element of" prompts that
perhaps sets)? Given two sets X and Y, they define the set of
functions X->Y; is that the operation you suggested?

If my interpretation is wrong, may I ask for amn example? In the
analogies that I brought in the root message I could, for example,
explain how universal quantifier works on domain of three elements
x={1,2,3}, that is how we do conjunction P(1) ^ P(2) then amend the
expression to (P(1) ^ P(2)) ^ P(3) this is how Ax.P(x) becomes a
proposition. Can you draw a similar venue for lambda abstraction?

> > In binary form -- exp(x,y) --
> > exponentiation is not associative, that would also disqualify it.
>
> why do you think an operation must be associative?

Because all the other analogies (sum, product, and predicate logic
quantifiers) have this property?

On Sep 6, 7:14*pm, Tegiri Nenashi <TegiriNena...@gmail.com> wrote:
> On Sep 6, 6:34*pm, galathaea <galath...@gmail.com> wrote:
> > why do you think an operation must be associative?
>
> Because all the other analogies (sum, product, and predicate logic
> quantifiers) have this property?

Better argument may be that if operation is not associative, then,
when applied iteratively the result is no longer well defined. Sure
with non associative operation '*' the expression a * b * c is
ambiguous!

On Sep 6, 7:14 pm, Tegiri Nenashi <TegiriNena...@gmail.com> wrote:
> On Sep 6, 6:34 pm, galathaea <galath...@gmail.com> wrote:
> > On Sep 6, 6:03 pm, Tegiri Nenashi <TegiriNena...@gmail.com> wrote:
> > > On Sep 6, 3:31 pm, galathaea <galath...@gmail.com> wrote:

> > > > if i understand what you mean by lambda quantifier
> > > > (as in the standard form on which eval's work through application
> > > > e.g. lambda calculus lambdas
> > > > with their well known universal properties)
> > > > then i would expect the exponential to be the corresponding operation
> > > > in other words
> > > > given a objects X and Y
> > > > a function f from X to Y is an element of the exponential object
>
> > > > X
> > > > f elementOf Y
>
> > > > and the evaluation at an element of X is given by
>
> > > > X
> > > > eval: Y x X --> Y
>
> > > > (such that a variety of commutative diagrams obtain)
>
> Could you please be more specific what algebraic structure you have in
> mind? Specifically, what are the elements ("element of" prompts that
> perhaps sets)? Given two sets X and Y, they define the set of
> functions X->Y; is that the operation you suggested?

i'm talking about the standard categorial exponentiation

in the category of set
it's as you describe

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

> If my interpretation is wrong, may I ask for amn example? In the
> analogies that I brought in the root message I could, for example,
> explain how universal quantifier works on domain of three elements
> x={1,2,3}, that is how we do conjunction P(1) ^ P(2) then amend the
> expression to (P(1) ^ P(2)) ^ P(3) this is how Ax.P(x) becomes a
> proposition. Can you draw a similar venue for lambda abstraction?

of course

it's the modern foundations of computer science

it's why compsci works in cartesian closed categories
to define things like domain theory and denotational semantics

amadio and curien have what has been my favorite book on this
"domains and lambda calculi"
though many advanced compsci overviews
will lay the same foundations

> > > In binary form -- exp(x,y) --
> > > exponentiation is not associative, that would also disqualify it.
>
> > why do you think an operation must be associative?
>
> Because all the other analogies (sum, product, and predicate logic
> quantifiers) have this property?

lambda is nonassociative though
(commonly written in left-associative notation)

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

Tegiri Nenashi <TegiriNenashi@gmail.com> wrote:
> Observation: all quantuifiers correspond to some binary algebraic
> operation. Consider:

Or more precisely: Four commonly known "big operations" (which are not
quantifiers in the strict sense) happen to express "folds" (or
reductions, or whatever you like to call them) based on binary
operations. Forall- and existential quantification can be seen like
this, too, but only if you reduce them to operations on truth-values.

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).

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

> 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?

There is none in the sense you're looking for.

Perhaps a better way to think about it is:

1) A "capital-sigma" sum over some expression using x considers that
expression as a function f : X -> Y, where X is finite and Y admits a
binary operation "plus", and then folds it.
2) Same for "capital-pi" product.
3) Same for lattice supremum and infimum over finite sets.

In the case where X is infinite, it get's more complicated. Then
additionally to the binary operation there must either be some form of
limit on Y, or you treat the "capital" operation as the primitive
in the first place, and define the binary operation as special case.

In the above scheme, you can think of the lambda is only doing the
"treat the expression as a function" part, without the following fold.

There are also other operators which bind a variable and are not based
on some binary operation, for example

- Recursive types, using the small greek letter mu. For example,

mu x. (1 + a * x)

is the type of lists over a.

- New names. For example in the pi-calculus, the small greek letter nu
introduces a new name.

And more (e.g. the small greek letter pi in the pi-calculus I just mentioned).

The exponential construction "galathea" (I recommend to google for
some other posts by this author to get some idea what kind of things
he/she normally writes) mentions operates *on* types: When taking
an expression as function f : X -> Y, one can write the whole function
space as Y^X. That is *not* what you're looking for, because you're
asking for a binary function "inside" Y.

BTW, the reason for this notation is that if you write the categorical
product (for sets, pair-construction) as X * Y and the categorical sum
(for sets, disjoint union) as X + Y, and the category is nice, then you
get equivalences like

Z^(X+Y) = Z^X * Z^Y

If you're confused by all this, just ignore it :-) The important part
is: The lambda-notation doesn't involve any binary operation.

- Dirk

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" (which are not
> quantifiers in the strict sense) happen to express "folds" (or
> reductions, or whatever you like to call them) based on binary
> operations. Forall- and existential quantification can be seen like
> this, too, but only if you reduce them to operations on truth-values.
>
> 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).
>
> And what about differentiation? It's the inverse operation of
> integration, so what binary operation should it correspond to? :-)

difference obviously
as any intro text to calculus will point out

> > 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?
>
> There is none in the sense you're looking for.
>
> Perhaps a better way to think about it is:
>
> 1) A "capital-sigma" sum over some expression using x considers that
> expression as a function f : X -> Y, where X is finite and Y admits a
> binary operation "plus", and then folds it.
> 2) Same for "capital-pi" product.
> 3) Same for lattice supremum and infimum over finite sets.
>
> In the case where X is infinite, it get's more complicated. Then
> additionally to the binary operation there must either be some form of
> limit on Y, or you treat the "capital" operation as the primitive
> in the first place, and define the binary operation as special case.
>
> In the above scheme, you can think of the lambda is only doing the
> "treat the expression as a function" part, without the following fold.
>
> There are also other operators which bind a variable and are not based
> on some binary operation, for example
>
> - Recursive types, using the small greek letter mu. For example,
>
> mu x. (1 + a * x)
>
> is the type of lists over a.
>
> - New names. For example in the pi-calculus, the small greek letter nu
> introduces a new name.
>
> And more (e.g. the small greek letter pi in the pi-calculus I just mentioned).
>
> The exponential construction "galathea" (I recommend to google for
> some other posts by this author to get some idea what kind of things
> he/she normally writes) mentions operates *on* types: When taking
> an expression as function f : X -> Y, one can write the whole function
> space as Y^X. That is *not* what you're looking for, because you're
> asking for a binary function "inside" Y.

no

actually the space here
on which the functional view you use above is defined
is a _function_ space here

the function X -> Y i am discussing
is the Y _you_ are discussing
just as the Y _you_ use
would be product or coproduct spaces
(except that
to be consistent with categorial usage
the existential quantifier is over X)

to make it even more explicit
these are all adjoint relations in a category
functoring terms
(yes terms!)
to corresponding categorial constructions

there are existential quantifier adjoints
and universal quantifier adjoints
and
yes
exponential adjoints

the curry-howard isomorphism
for instance
gives the following table of connections:

logic type theory category theory
----- ----------- ---------------
true unit terminal object
false void initial object
conjunction products products
disjunction unions coproducts
implication functions exponentials

kwarc.info/teaching/CompLog/florian4.pdf

but in general
yes
it's a good idea to build trust networks
by learning the history of one giving advice

of course
if one is giving responsible advice
one would suggest _relevant_ searches
using keywords to pick out contributions in the topic being discussed

for instance
one might want to see discussions i have had
on orthomodular lattices and quantum logic
or denotational and operational semantics
or
if interested in mathematical competence
maybe my generalised trigonometry
and multisection theorems on (q-)hypergeometrics

if one is interested in my poetry
or philosophy
or politics
or my experimental electronica
then by all means feel free to explore
(and satisfy my blatant narcissism)
but i doubt they will help form an opinion here

it's also good to compare with other posters who may
for instance
display poor reasoning skills
through use of fallacies like ad hominems...

> BTW, the reason for this notation is that if you write the categorical
> product (for sets, pair-construction) as X * Y and the categorical sum
> (for sets, disjoint union) as X + Y, and the category is nice, then you
> get equivalences like
>
> Z^(X+Y) = Z^X * Z^Y
>
> If you're confused by all this, just ignore it :-) The important part
> is: The lambda-notation doesn't involve any binary operation.

many other reasons exist

one big one is that the cardinality of the function space
is |Y|^|X|

which is
(wait for it...)
the same type of relationship of cardinalities
that lies behind the notations X + Y and X x Y
for the set coproducts and products
being discussed here!

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