Quantifier notation for operations that are merely associative; more on quantifiers

69 views
Skip to first unread message

Bastiaan Braams

unread,
Nov 19, 2018, 9:50:04 AM11/19/18
to Calculational Mathematics
This is to report on a convention that I've found useful in my own work. We are all familiar here with the notation <Op v: P(v): F(v)> to represent the application of the operation Op (associated with a binary operation op) to the bag of values F(v) obtained from the set {v: P(v)}. For this purpose operation Op (or op) needs to be associative and commutative and we like it or we demand that Op has a neutral element.
Often I want to use such notation for an operation that is associative but not necessarily commutative. I resisted that temptation, but since recently I am using it in my own notes with a slight modification: I put an arrow above the Op symbol. In TeX/LaTeX notation, I use \vec\Op as the operator symbol. Primarily I use this for a Cartesian product of sets and for tensor products of vectors or vector spaces. The domain specification P(v) must then define a set with a total order that is understood, and in my practice it is always an integer range. So we get something like <\vec\times k: 0\le k\lt d: X_k> for the Cartesian product of the sets X_k as k runs from 0 to d-1. I like this notation enough to recommend it here.
On the subject of quantifier notation, I recently came across a note by Lambert Meertens "Least Fixpoints Calculationally" (1998). (See his home page at Kestrel Institute.) Meertens discusses (inter alia) some issues of quantifiers applied to an infinite bag. In his approach, the quantifier Op defines uniquely the binary operation op, but not the other way around. I appreciated to see that.
Further on the subject of quantifier notation, I wonder what might be the most appropriate meaning of the expression <v: P(v): F(v)>, not containing any Op. It always seemed natural to me to let this define the bag of values F(v) associated with the set {v: P(v)}, especially as there is not otherwise a standard notation for defining a bag. However, Meertens (in the cited article or manuscript under the subheading "function comprehension") uses that notation (albeit with round brackets) to define a partial function F on the domain characterized by P. I appreciate that meaning too.

Diethard Michaelis

unread,
Nov 26, 2018, 6:13:35 AM11/26/18
to calculationa...@googlegroups.com, Bastiaan Braams
Hi Bastiaan,

(0) On quantifiers.

By induction
any binary operator op: T x T -> T
yields a quantifier OP
over finite segments [0,n) of naturals

OP([0,0):f) = "left neutral element".op, if such exists, or
OP([0,1):f) = f.0
OP([0,n+1):f) = OP([0..n):f) op f.n
[using "Meertens" point-free OP(r:f) for <OP d:r.d:f.d>]

Translation generalizes the index set (range) [0..n)
to arbitrary segments [a,a+n),
and order preserving transformation
to finite total orders as index set.

Such inductively quantified operators
already have a limited range of useful laws
including the one-point rule
but excluding range-splitting (= associativity).

Note: Addition of floating point numbers being not associative
makes such general quantifiers practically unavoidable.
Or see Gauss' quantifier notation for continued fractions.
End Note.

(1) On (range:function) notation and dummy-noise

As for the (range:function) notation for partial(ized) functions
thanks for the hint to the 1998 Meertens paper.

I had to discover such notation long ago for myself
as I wanted both point-free (= dummy-free) quantifiers
[the dummy and it's name just being noise]
and quantifiers as first class citizens.
So I asked what kind of object do quantifiers operate on?
A function together with a range = ... a partial function.
And Meertens' notation arose mostly by necessity.

All the best, Diethard.

Am 19.11.2018 um 15:50 schrieb Bastiaan Braams:
> This is to report on a convention that I've found useful in my own work. We
> are all familiar here with the notation <Op v: P(v): F(v)> to represent the
> application of the operation Op (associated with a binary operation op) to
> the bag of values F(v) obtained from the set {v: P(v)}. For this purpose
> operation Op (or op) needs to be associative and commutative and we like it
> or we demand that Op has a neutral element.
> Often I want to use such notation for an operation that is associative but
> not necessarily commutative. I resisted that temptation, but since recently
> I am using it in my own notes with a slight modification: I put an arrow
> above the Op symbol. In TeX/LaTeX notation, I use \vec\Op as the operator
> symbol. Primarily I use this for a Cartesian product of sets and for tensor
> products of vectors or vector spaces. The domain specification P(v) must
> then define a set with a total order that is understood, and in my practice
> it is always an integer range. So we get something like <\vec\times k: 0\le
> k\lt d: X_k> for the Cartesian product of the sets X_k as k runs from 0 to
> d-1. I like this notation enough to recommend it here.
> On the subject of quantifier notation, I recently came across a note by
> Lambert Meertens "Least Fixpoints Calculationally" (1998). (See his home
> page at Kestrel Institute <https://www.kestrel.edu/home/people/meertens/>.)
Reply all
Reply to author
Forward
0 new messages