Re: [mathmeth] Introduction, punctual functions

[Diethard Michaelis]

Hi Bas,

Some comments. Wanted to write earlier but ...

On naming:

(a) "punctual" is a name I disliked from the beginning. I still do not
know how to nicely translate it into German: "pünktlich" is definitely
wrong, "punktweise" (point wise) equally inappropriate. In a (probably)
unpublished paper [rutger20] "A Mathematical Approach to Logic", Aug.18
1994, Rutger M. Dijkstra uses "internal" for punctual predicate
transformers. That seems to be much better a choice: Punctuality of
predicate transformers is expressed by Boolean operators only and the
normal form theorem later tells us that punctual predicate transformers
themselves are those expressible by the Boolean operators.

(b) "linear". I choose "punctual = linear" because it refers to the
Boolean ring structure, (==,true,\/,false) = (+,0,*,1) and my proof of
it was entirely in terms of this Boolean ring. We have
f is a punctual pred transformer
<=> { def }
[(X == Y)\/(f.X == f.Y) == f.X == f.Y] for all preds X,Y
<=> { (==,true,\/,false) = (+,0,*,1) ; [] = (=0) }
(X + Y)*(f.X + f.Y) + f.Y + f.X = 0
<=> { algebra ; (+) = (-) }
f.X*(X + Y + 1) + f.Y*(X + Y + 1) = 0
Substituting 0 and 1 for Y yields 2 linear equations for unknown f.X.
Subtracting (= adding) both equations yields
f.X + f.0*(X + 1)
+ f.1*X = 0
<=> { rearrange }
f.X + f.0 + X*(f.0 + f.1) = 0
and we are done.

On point free quantifiers
(the only point free quantifier in the DS book is []).
Not your subject here, but you might like it.
Paul Halmos, Algebraic Logic, 1962 gives a point free characterisation
of quantifiers as (non punctual) operators on Boolean Algebras.
The 3 defining properties (rewritten for universal quantifier []) are
[true],
[p] => p,
[p \/ [q]] = [p] \/ [q].
The chapter / paper on point free quantifiers is
Algebraic logic, I. Monadic boolean algebras
which is directly accessible
http://www.numdam.org/item?id=CM_1954-1956__12__217_0
http://www.numdam.org/article/CM_1954-1956__12__217_0.pdf
I've studied point free quantifiers years ago. Presentation of
quantifier theory profits a lot from a point (= dummy) free style.

Diethard.

Am 06.07.2017 um 13:18 schrieb Bastiaan Braams:
> Meanwhile I have found earlier references for that normal form for punctual
> functions (or rather: punctual predicate transformers). Lemma 6 in
> [Bijlsma, 1993, ab45] gives the normal form. Bijlsma writes that the result
> first appeared in [Wiltink et al., 1985]. I don't have access to that
> reference.
>
> [Bijlsma, 1993, ab45] Lex Bijlsma: "Punctuality, conjunctivity, and
> monotonicity." Report AB45, December 1993, Unpublished. See
> http://www.open.ou.nl/lby/ab45.pdf or see under http://www.open.ou.nl/lby/.
>
> [Wiltink et al., 1985] J. G. Wiltink, R. W. Bulterman, W. H. J. Feijen, A.
> Kaldewaij, Cai Chengdian, M. Boasson, A. Bijlsma, and A. J. M. van
> Gasteren: "A note on propositional predicate transformers." Eindhoven
> University of Technology, January 1985.
>
> Bas Braams
>
> On Monday, July 3, 2017 at 2:13:27 PM UTC+2, Bastiaan Braams wrote:
>>
>> Being new on this group I start with a brief introduction. As a student in
>> mathematics and informatics in Eindhoven 1972-1976 my programme included
>> classes from Edsger Dijkstra and tutorials from Wim Feijen. I also
>> participated in the Eindhoven Tuesday Afternoon Club for some months in
>> 1976, but then I switched to Utrecht and completed my studies in
>> theoretical physics. After the Ph.D. I moved to the USA for a post-doc at
>> Princeton Plasma Laboratory and I had research positions at Courant
>> Institute (NYU) and at Emory University, working in different areas of
>> computational science. From 2009-2016 I was in research management at IAEA
>> in Vienna. Now I am back in the Netherlands and I have a guest appointment
>> at Centrum Wiskunde & Informatica (CWI), the Dutch national research centre
>> for mathematics and computing science. I kept up with the EWD series while
>> it lasted and generally retained a practical interest in programming
>> methodology and calculational mathematics.
>>
>> Recently I came across the www.mathmeth.com web site and this news group
>> and it was an occasion for me to look more closely at the Calculational
>> Mathematics collection of articles that is linked at
>> www.mathmeth.com/read.shtml. The notation and style is all familiar to
>> me, but I had not spent much time previously studying the precise
>> mathematical development. As I am reading through this collection more
>> closely I make clarifying notes to myself. Here is one such note, on the
>> subject of punctual functions. I am following EWD 1123 for definitions and
>> notation.
>>
>> == Normal form for punctual functions ==
>>
>> Punctual functions (on some set of predicates or boolean structures that
>> is taken for granted) are defined as functions f satisfying
>>
>> (0) <∀x,y:: [ (x ≡ y) ⇒ (f.x ≡ f.y) ]>
>>
>> In EWD 1123, pp. 24-25, it is noted and proved that
>>
>> (i) The identity function is punctual;
>> (ii) The negation of a punctual function is punctual;
>> (iii) An existential quantification over punctual functions is punctual.
>>
>> I am missing the constant functions in that enumeration and to clarify
>> things for myself I use a different list as a starting point:
>>
>> (i') Constant functions are punctual;
>> (ii') The identity function is punctual;
>> (iii') Functions formed from punctual functions by applying the elementary
>> operations of predicate calculus are punctual.
>>
>> (I believe that "elementary operations" will generally be understood as
>> those generated by negation and conjunction, so not including universal or
>> existential quantification.) Let me skip the direct proof for present
>> purposes; the proof will be implicit in what follows anyway.
>>
>> Repeated application of the rules (i')-(iii') can generate arbitrarily
>> long expressions, but they can all be simplified into a conjunctive or
>> disjunctive normal form as follows:
>>
>> (1) f.x = (x∨s) ∧ (¬x∨t)
>> (2) f.x = (x∧t) ∨ (¬x∧s)
>>
>> for arbitrary constants s and t.
>>
>> I will show first that the two representations provide the same function.
>> For arbitrary x, s and t:
>>
>> (x∨s) ∧ (¬x∨t)
>> = {distributive law, removing a trivial term x∧¬x}
>> (x∧t) ∨ (¬x∧s) ∨ (s∧t)
>> = {splitting s∧t over x (distributive law)}
>> (x∧t) ∨ (¬x∧s) ∨ (x∧(s∧t)) ∨ (¬x∧(s∧t))
>> = {absorption applied twice}
>> (x∧t) ∨ (¬x∧s)
>>
>> Functions constructed according to rules (i') and (ii') can obviously be
>> put in the form (1) or (2); for the constant functions (say constant c) let
>> s=c and t=c, and for the identity function let s=*false* and t=*true*. To
>> show that (1) or (2) (with arbitrary s and t) is indeed a normal form for
>> the rules (i')-(iii') only rule (iii'') needs a bit of work. Negation is
>> easy, following de Morgan's laws it just converts a function of form (1)
>> into one of form (2) and vice versa, of course with different constants.
>> For the case of conjunction, take two functions written in the form (1),
>> say with constants (s,t) and (s',t'), write out the conjunction, and use
>> that (x∨s) ∧ (x∨s') = x∨(s∧s') and (¬x∨t) ∧ (¬x∨t') = ¬x ∨ (t∧t') (the
>> distributive property).
>>
>> So (1) or (2) can serve as a normal form for a broad class of punctual
>> functions. What about the other direction?
>>
>> Let f be a punctual function and let s = f.*false*, t = f.*true*. We
>> calculate from the definition.
>>
>> <∀x,y:: [ (x ≡ y) ⇒ (f.x ≡ f.y) ]>
>> ≡ {write the antecedent in disjunctive form and the consequent in
>> conjunctive form}
>> <∀x,y:: [ (x∧y) ∨ (¬x∧¬y) ⇒ (f.x∨¬f.y) ∧ (¬f.x∨f.y) ]>
>> ≡ {split the antecedent and the consequent over the implication}
>> <∀x,y:: [ (x∧y ⇒ f.x∨¬f.y) ∧ (¬x∧¬y ⇒ f.x∨¬f.y) ∧ (x∧y ⇒ ¬f.x∨f.y) ∧
>> (¬x∧¬y ⇒ ¬f.x∨f.y) ]>
>> ≡ {everywhere operator distributes over conjunction and universal
>> quantification distributes over conjunction}
>> <∀x,y:: [ x∧y ⇒ f.x∨¬f.y ]> ∧ <∀x,y:: [ ¬x∧¬y ⇒ f.x∨¬f.y ]> ∧ <∀x,y:: [
>> x∧y ⇒ ¬f.x∨f.y ]> ∧ <∀x,y:: [ ¬x∧¬y ⇒ ¬f.x∨f.y ]>
>> ⇒ {instantiate each quantified expression with either true or false for y,
>> whichever gives the nontrivial result, and recall s = f.*false*, t = f.
>> *true*}
>> <∀x:: [ x ⇒ f.x∨¬t ]> ∧ <∀x:: [ ¬x ⇒ f.x∨¬s ]> ∧ <∀x:: [ x ⇒ ¬f.x∨t ]> ∧
>> <∀x:: [ ¬x∧ ⇒ ¬f.x∨s ]>
>> ≡ {the shunting rule of implication}
>> <∀x:: [ x∧t ⇒ f.x ]> ∧ <∀x:: [ ¬x∧s ⇒ f.x ]> ∧ <∀x:: [ x∧¬t ⇒ ¬f.x ]> ∧
>> <∀x:: [ ¬x∧¬s ⇒ ¬f.x ]>
>> ≡ {take the contrapositive where we have ¬f.x as the consequent}
>> <∀x:: [ x∧t ⇒ f.x ]> ∧ <∀x:: [ ¬x∧s ⇒ f.x ]> ∧ <∀x:: [ f.x ⇒ ¬x∨t ]> ∧
>> <∀x:: [ f.x ⇒ x∨s ]>
>> ≡ {universal quantification over conjunction, everywhere operator over
>> conjunction}
>> <∀x:: [ (x∧t ⇒ f.x) ∧ (¬x∧s ⇒ f.x) ∧ (f.x ⇒ ¬x∨t) ∧ (f.x ⇒ x∨s) ]>
>> ≡ {rules of implication}
>> <∀x:: [ ((x∧t) ∨ (¬x∧s) ⇒ f.x) ∧ (f.x ⇒ (¬x∨t) ∧ (x∨s)) ]>
>> ≡ {use that (x∧t) ∨ (¬x∧s) = (¬x∨t) ∧ (x∨s), then replace a pair of
>> converse implications by an equivalence}
>> <∀x:: [ f.x ≡ (x∧t) ∨ (¬x∧s) ]>
>> ≡ {again use (x∧t) ∨ (¬x∧s) = (¬x∨t) ∧ (x∨s)}
>> <∀x:: [ f.x ≡ (¬x∨t) ∧ (x∨s) ]>
>>
>> So any punctual function f can be written in the form (1) or (just as
>> well) (2), with s=f.*false* and t=f.*true*. In the above proof one step
>> is an implication instead of an equivalence, but by closing the circle we
>> know that that implication is really an equivalence.
>>
>> I think that in the language of boolean algebra these functions may be
>> called inhomogeneous polynomials of one variable. I am not sure of this.
>>
>> == Alternate characterization of punctual functions ==
>>
>> The characterization of punctual functions through the normal form
>> provides an alternative definition of punctuality: function f is punctual if
>>
>> (3) <∀x:: [ f.x ≡ (x∧f.*true*) ∨ (¬x∧f.*false*) ]>
>>
>> or equivalently if
>>
>> (3') <∀x:: [ f.x ≡ (¬x∨f.*true*) ∧ (x∨f.*false*) ]>
>>
>> Relative to the definition (0) we have removed one variable from the
>> quantifier, but of course we have lost the obvious connection to the
>> Leibniz property, and in fact it doesn't look so easy to apply (3) or (3')
>> in practice. A cleaner single variable characterization is obtained by
>> going back a few steps in the proof of the normal form: function f is
>> punctual if and only if:
>>
>> (4) <∀x:: [ (x∧f.*true* ⇒ f.x) ∧ (¬x∧f.*false* ⇒ f.x) ∧ (f.x ⇒ ¬x∨f.*true*)
>> ∧ (f.x ⇒ x∨f.*false*) ]>
>>
>> or equivalently, by shunting in the implications, if and only if:
>>
>> (4') <∀x:: [ (x ⇒ f.x∨¬f.*true*) ∧ (¬x ⇒ f.x∨¬f.*false*) ∧ (f.x∧¬f.*true*
>> ⇒ ¬x) ∧ (f.x∧¬f.*false* ⇒ x) ]>
>>
>> To me the forms (4) or (4') look easier to apply than either (0) or (3) or
>> (3').
>>
>> == "Punctual is linear" ==
>>
>> I see that the topic of punctual functions came up on this newsgroup on
>> one earlier occasion, in 2007 in the conversation An experiment in
>> simplification
>> <https://groups.google.com/forum/#!topic/calculational-mathematics/sIwfDsw8L2w>
>> in a message from Diethard Michaelis through Jeremy Weissmann; reference is
>> made there to EWD 1187, Boolean connectives yield punctual expressions
>> <https://www.cs.utexas.edu/users/EWD/ewd11xx/EWD1187.PDF>. With (4) in
>> mind I would characterize that "punctual is linear" property by the
>> following dual pair:
>>
>> (5) <∀x:: [ x⇒f.*true* ≡ x⇒f.x ]>
>> (5') <∀x:: [ f.x⇒¬x ≡ f.*false*⇒¬x ]>
>>
>> Let us show that (5) is equivalent to one pair of conjuncts of (4) and
>> (5') is equivalent to the other pair. (We keep in mind that the everywhere
>> operator distributes over conjunction and universal quantification
>> distributes over conjunction.) For any x:
>>
>> x⇒f.*true* ≡ x⇒f.x
>> = {mutual implication}
>> ((x⇒f.*true*) ⇒ (x⇒f.x)) ∧ ((x⇒f.x) ⇒ (x⇒f.*true*))
>> = {use the rule, obtained just for this occasion, that (x⇒a)⇒(x⇒b) =
>> ¬x∨¬a∨b}
>> (¬x∨¬f.*true*∨f.x) ∧ (¬x∨¬f.x∨f.*true*)
>> = {change a disjunction to an implication, twice}
>> (x∧f.*true* ⇒ f.x) ∧ (f.x ⇒ ¬x∨f.*true*)
>>
>> and
>>
>> f.x⇒¬x ≡ f.*false*⇒¬x
>> = {mutual implication}
>> ((f.x⇒¬x) ⇒ (f.*false*⇒¬x)) ∧ ((f.x⇒¬x) ⇒ (f.*false*⇒¬x))
>> = {now use the rule (a⇒¬x)⇒(b⇒¬x) = a∨¬b∨x}
>> (f.x∨¬f.*false*∨x) ∧ (f.*false*∨¬f.x∨x)
>> = {change a disjunction to an implication, twice}
>> (¬x∧f.*false* ⇒ f.x) ∧ (f.x ⇒ x∨f.*false*)
>>
>> Therefore punctual functions satisfy (5) and (5') and a function that
>> satisfies both (5) and (5') is punctual. But I think that the
>> characterization (4) is easier to apply in practice.
>>
>> Bas Braams
>> Centrum Wiskunde & Informatica (CWI), Amsterdam
>>
>>
>