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