On Sep 6, 11:50 pm, Dirk Thierbach
wrote:
> Tegiri Nenashi
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
