The Problem

This page describes the problem I have had for a long time, at least in one facet or another.

Setting

There is a multiset read operation, which is the only way to observe a document:

\[ d(p) \]

Consequently, it is the only operation being affected by document manipulations, namely update and delete:

\[ d[p \rightarrow v] \qquad \mbox{and}\qquad d[p \rightarrow] \]

To get rid of these two special operations, we only have to look at the combination of such with a read opertation, i.e.

\[ d[p \rightarrow v](q) \qquad\mbox{and}\qquad d[p \rightarrow](q) \]

The process of eliminating the manipulation is therefore a transformation of the general form:

\[ d[p \rightarrow v_? ](q) = E\;[p,\; d(q),\; v_?] \]

The manipulation is gone and the result is some expression depending only on $p$, $d(q)$ and possibly some value $v$.

External Uniqueness Argument

This argument is based on the semantics of the enclosing operator.

In general, there are two main situations in which document reads - which are value multisets - can appear:

In a context where a unique value is expected, maybe even a unique value of a certain type.
In a context where a general multiset is enough, if restricted to a specific type, it will just be filtered down.

If we can establish a formula is safe, the replacement operation can just assume these properties are fulfilled, i.e.

The semantics of the expression is a singleton of correct type.
The semantics is a general multiset, i.e. no useful assumptions.

Safety can be established if the formula does not contain conditionals (strict), does not use multiset difference (difree) or other multiset operations on paths (opfree). Strictness can always be established for free.

Internal Uniqueess Argument

This argument is based on the semantics of the operator itself.

We can differentiate two categories of reads:

The read operation contains a general path, i.e. there is a document and there are parameters (constituting parameter environment $R$), for which the semantics of the path expression yields a true multiset, not just a singleton or an empty set. \[ \parallel p\parallel_R = q_* \] The read operation itself might yield a singleton only, however, we don't know. \[ \parallel d(p)\parallel_R = \{\} \qquad\mbox{or}\qquad \parallel d(p)\parallel_R = \{v\} \qquad\mbox{or}\qquad \parallel d(p)\parallel_R = v_* \]
The path in the read operation is statically unique, i.e. for all documents and parameters, it can only yield either the empty set or a singleton set. \[ \parallel p\parallel_R = \{\} \qquad\mbox{or}\qquad \parallel p\parallel_R = \{q\} \] The read operation consequently is also statically unique. \[ \parallel d(p)\parallel_R = \{\} \qquad\mbox{or}\qquad \parallel d(p)\parallel_R = \{v\} \] Note that there is no one to one correspondence, as the read can still yield the empty set, even if the path is a singleton.

Elimination

As far as elimination is concerned, we now get four combinations, as safety makes the external uniqueness argument statically exploitable.

Case: Both Arguments

We know the read is externally and internally unique.

Prerequisites for the term $d[p \rightarrow v_?](q)$:

$p$ is unique, as both manipulations would not have semantics otherwise.
$q$ is at most a singleton, cause of statical uniqueness.
$q$ is at least a singleton, as otherwise the read would always result in an empty set, regardless of $d$ or the manipulation.
- As the whole term has a singleton semantics, cause of external uniqueness, this can not be.

This means the update operation can be transformed as follows, as $p$ and $q$ are exact singletons:

\[ d[p \rightarrow v](q) \quad=\quad \mbox{if}\quad p \in q \quad\mbox{then}\quad v \quad\mbox{else}\quad d(q) \quad\mbox{fi} \]

We can't just use equality here, as we don't have equality on paths… although both are exactly uniques, which would make it possible.

The delete operation is also quite easy, as we only have to check if the $q$ appears in the descendant set, which can be done with a simple count.

\[ d[p \rightarrow](q) \quad=\quad \mbox{if}\quad q \in \mbox{intersect}\;\;q\;\;p \quad\mbox{then}\quad \{\} \quad\mbox{else}\quad d(q) \quad\mbox{fi} \]

Note here, that this only works, because we can count the singleton path $q$, otherwise the count might not have semantics. Also, the count operation needs an expression describing the descendant set, which is only possible as cutting it with the update path $p$ can be done syntactically!

Case: Only Externally Unique

This is an interesting case. The path expression does not necessarily return a singleton, yet the whole read operation (with manipulation) returns one. The manipulation is also the greatest problem here.

Which path was - in the end - the one responsible for the one value? And was the document modified at this path or not, etc.

I think I can transform every such occurrence into an equivalent formula, which contains a statically unique term, with a guard using an aggregate. The guard therefore no longer assumes or needs the original term to be unique, so the external argument gets dropped. We therefore fall into the other two cases, as we have both arguments at the original term and none in the guard, yet the guard uses an aggregate.

Another option would be to just forbid the combination and assume the user writes statically unique code where a unique value is expected by the context. (Note that a stronger typed version of the theory would have been able to just forbid the case, yet it would have the old problems of exception handling and partial semantics.)

Case: No Usable Argument

If we don't need an exact singleton, static uniqueness is not that helpful, as it can still result in an empty set. This would be ok for updates, but useless for deletes. Also this is a situation which doesn't make too much sense and we definitely do not want to force it. This means terms dynamically yielding a multiset have to be handled differently and the remaining two cases collapse.

We can eliminate the manipulations by replacing them with a multiset difference, as well as other multiset operators in the update case:

\[ d[p \rightarrow v](q) \quad=\quad \mbox{count}\;\;q\;\;p \;\otimes\; v \;\;\oplus\;\; d(q \;\ominus\; \mbox{count}\;\;q\;\;p \times p)\]

\[ d[p \rightarrow](q) \quad=\quad d(q \;\ominus\; \mbox{intersect}\;\;q\;\;p)\]

We will see, that the read operation now has to be contained in an aggregate or we can't get rid of the introduced operations.

Normalization

To execute the first elimination, safety is required. The precondition of every formula and program, which are strict, difree and opfree, can be made safe. So if we start with these properties, we are able to do the eliminations. To be able to incrementally simplify - and for reasons of a clean abstract syntax - we don't want to introduce any of the above while eliminating manipulations.

We therefore are interested in normalized formulas, i.e. formulas which are strict, difree and opfree.

The first elimination only introduces conditionals, which can always be eliminated without side condition. The second elimination, however, introduces all three. Again, conditionals are not the issue, so multiset operations and in particular the multiset difference have to be considered.

Idea

The basic idea now is to demand generic read operations only to be contained in aggregates¹⁾. Let's start with a formula with this property. I now have to show, that I then can eliminate the multiset difference and other operations, which I create by eliminating the document manipulations.

The important part is what containment means. We can not define it as direct containment, as the general read can, for example, be contained in a path, which is again used in a read, which then is contained in an aggregate. This means I have to drag the operation “all the way up” to the aggregate and have to make sure there actually is one.

So what does “general reads are only contained - maybe only indirectly - in an aggregate” mean? And how do I describe the pull out operation? I have seen with the conditional example, that this can get technically ugly.

Abstract Syntax

So lets revise the abstract syntax:

Type	Constructor	Parameter	Parameter	Remark	Unique
value	Val value			leaves	Yes
	Var name
	Con name
	Sum	value (*, I)		aggregates	Yes
	Size	value (*)
	Tally type	value (*)
	Count	value (*)	value (1)
	Scal	value (1, I)	value (-, I)	operator	maybe
	Read doc	path (-)		mutual	maybe
	VPlus	value (*)	value (*)	operators	No
	VRep	value (1, I)	value (*)	operators	No
	VCond lit	value (-)	value (-)	strict	maybe
path	PRoot			leaf	Yes
	Path label	path (-)	value (-, D)	mutual	maybe
	Kind label	path (*)		paths	No
	PPlus	path (*)	path (*)	operators
	PRep	value (1, I)	path (*)	operators
	Diff	path (*)	path (*)	difference
	PCond lit	path (-)	path (-)	strict	maybe
doc	Dollar			leaf	-
	Upd doc	path (1)	value (1)	uniques
	Del doc	path (1)		uniques
	DCond lit doc doc			strict
pred	Equal	value (1)	value (1)	uniques
	Rel bool	value (1)	value (1)	uniques
	RCond lit pred pred			strict
lit	L bool pred			decoration

Containment

If we restrict ourselves to true multisets, i.e. where the external uniqueness argument does not apply, we get a slightly restricted set of containment relations.

Diagram

Sum $\circ$

Tally t $\circ$

Read d $\circ$

Scal n $\circ$

VRep n $\circ$

VCond $\circ$ b

Size $\circ$

Count $\circ$ p

VPlus $\circ$ b

VPlus a $\circ$

VCond a $\circ$

Path p $\circ$

PPlus $\circ$ b

PPlus a $\circ$

PCond $\circ$ b

Path $\circ$ i

Kind $\circ$

Diff $\circ$ b

Diff a $\circ$

PRep n $\circ$

PCond a $\circ$

Verdict

A read or any other value multiset can be contained in
- aggregates, which is fine already (leaf case)
- multiset operations and conditionals (direct recursion)
- paths as identifiers, which changes the type (mutual recursion)
A path or any other path multiset can in turn be contained in
- a read again, closing the loop (mutual recursion)
- other paths, a diff, other multiset operations or a conditional (direct recursion)

Simplified Diagram

Read d $\circ$

Ops/Cond

Aggr

Path p $\circ$

Paths

Diff

Ops/Cond

Predicates

So what do we get from all this? We are talking about two worlds:

The one of uniqueness, i.e. operators which expect unique values and expressions whose semantics is always at most a unique value. This could have been expressed with a stronger type system, but would have introduced a lot of problems which I explicitly solved by not using such a type system.
The one of true multisets, i.e. operations taking and yielding multisets, which are finally contained in an aggregate.

So the first predicate has to state the operators assuming they get unique values only contain statically unique expressions and that's that. Unfortunately, its not that easy…

Dragging

By eliminating the operations from the multiset world, we drag them – in the end – over aggregates, into the uniqueness world. This seems to be a problem, yet it is fairly obvious, that they still maintain uniqueness:

Scal remains itself, but gets a unique value as argument and maintains this property.
VRep will become a scalar multiplication of a unique value.
VPlus will be wrapped with an additional Sum when dragged out.

The relevant combinations are:

	res	Scal ($n\odot m$)			VRep ($n\otimes m$)			VPlus ($a\oplus b$)
Sum $\circ$	$v$	$\mbox{Sum}\;(n\odot m) $	$\equiv$	$ n\odot\mbox{Sum}\;m $	$\mbox{Sum}\;(n\otimes m) $	$\equiv$	$ n\odot\mbox{Sum}\;m $	$\mbox{Sum}\;(a \oplus b) $	$\equiv$	$ \mbox{Sum}\;(\mbox{Sum}\;a \oplus \mbox{Sum}\;b) $
Size $\circ$		$\mbox{Size}\;(n\odot m) $	$\equiv$	$ \mbox{Tally}\;\mbox{TInt}\; m$	$\mbox{Size}\;(n\otimes m) $	$\equiv$	$ n\odot\mbox{Size}\;m $	$\mbox{Size}\;(a \oplus b) $	$\equiv$	$ \mbox{Sum}\;(\mbox{Size}\;a \oplus \mbox{Size}\;b) $
Tally t $\circ$		$\mbox{Tally}\;\mbox{TInt}\;(n\odot m) $	$\equiv$	$ \mbox{Tally}\;\mbox{TInt}\;m$	$\mbox{Tally t}\;(n\otimes m) $	$\equiv$	$ n\odot\mbox{Tally t}\;m $	$\mbox{Tally}\;t\;(a \oplus b) $	$\equiv$	$ \mbox{Sum}\;(\mbox{Tally}\;t\;a \oplus \mbox{Tally}\;t\;b) $
Tally t $\circ$		$\mbox{Tally}\;t\;(n\odot m) $	$\equiv$	$ 0$	$\mbox{Tally t}\;(n\otimes m) $	$\equiv$	$ n\odot\mbox{Tally t}\;m $	$\mbox{Tally}\;t\;(a \oplus b) $	$\equiv$
Count $\circ$ p		$\mbox{Count}\;(a \odot (b \odot m)))\;v $	$\equiv$	$ \mbox{Count}\;((a \odot b) \odot m)\;v$	$\mbox{Count}\;(n\otimes m)\;v $	$\equiv$	$ n\odot\mbox{Count}\;m\;v $	$\mbox{Count}\;(a \oplus b)\;v $	$\equiv$	$ \mbox{Sum}\;(\mbox{Count}\;a\;v \oplus \mbox{Count}\;b\;v) $
Count $\circ$ p		$\mbox{Count}\;(a \odot (b \odot m)))\;v $	$\equiv$	$ \mbox{Count}\;((a \odot b) \odot m)\;v$	$\mbox{Count}\;(a \odot (n \otimes m))\;v $	$\equiv$	$n \odot \mbox{Count}\;(a \odot m)\;v$	$\mbox{Count}\;(n \odot (a \oplus b))\;v $	$\equiv$	$\mbox{Sum}\;(\mbox{Count}\;(n\odot a)\; v \oplus \mbox{Count}\;(n\odot b)\;v)$
Path p $\circ$	$p$	$p/l[n\odot m] $	$\equiv$	$ \{\}$	$p/l[n\otimes m] $	$\equiv$	$ n\otimes p/l[m]$	$p/l[a\oplus b] $	$\equiv$	$ p/l[a]\oplus p/l[b]$

	res	Diff ($a\ominus b$)			PRep ($n\otimes m$)			PPlus ($a\oplus b$)
Read d $\circ$	$v$/$v$	$\mbox{Sum}\;d(a\ominus b) $	$\equiv$	$ \mbox{Sum}\;d(a) - \mbox{Sum}\;d(b)$	$d(n\otimes m) $	$\equiv$	$ n\otimes d(m)$	$d(a\oplus b) $	$\equiv$	$ d(a)\oplus d(b)$
		$\mbox{Size}\;d(a\ominus b) $	$\equiv$	$ \mbox{Size}\;d(a) - \mbox{Size}\;d(b)$
		$\mbox{Tally}\;t\;d(a\ominus b) $	$\equiv$	$ \mbox{Tally}\;t\;d(a) - \mbox{Tally}\;t\;d(b)$
		$\mbox{Count}\;d(a\ominus b)\;v $	$\equiv$	$ \mbox{Count}\;d(a)\;v - \mbox{Count}\;d(b)\;v$
		$\mbox{Count}\;(n\odot d(a\ominus b))\;v $	$\equiv$	$ \mbox{Count}\;(n\odot d(a))\;v - \mbox{Count}\;(n\odot d(b))\;v$
	$p$	$p/l[d(a\ominus b)] $	$\equiv$	$ p/l[d(a)]\ominus p/l[d(b)]$
Path $\circ$ i		$(a\ominus b)/l[i] $	$\equiv$	$ a/l[i]\ominus b/l[i]$	$(n\otimes p)/l[i] $	$\equiv$	$ n\otimes p/l[i]$	$(a\oplus b)/l[i] $	$\equiv$	$ a/l[i]\oplus b/l[i]$
Kind $\circ$		$(a\ominus b)/l $	$\equiv$	$ a/l\ominus b/l$	$(n\otimes p)/l $	$\equiv$	$ n\otimes p/l$	$(a\oplus b)/l $	$\equiv$	$ a/l\oplus b/l$

Where the minus on value multisets is the integer minus aggregate:

\[a - b \equiv \mbox{Sum}\;(a\oplus (-1\odot b)) \]

In the end I will have to leave the Scal I guess, so I can't just say No in uve (which I don't…). But then I have a predicate which separates the worlds.

Based on this predicate I can go on eliminating the operations, I guess it has to be done in mutual recursion, which leads to the next predicate.

The Result

I have finally proven a first version of the big picture:

\[ \mbox{wip}\;\;P\;\;s\;\equiv\;(\mbox{normalize}\;\circ\;\mbox{strictify}\;\circ\;\mbox{core}\;\circ\;\mbox{secure})\;(\mbox{wp}\;\;P\;\; s) \]

\[ \mbox{nice_program}\;\; P\;\; s \quad\Longrightarrow\quad \models \{\mbox{wip}\;\; P\;\; s\}\; s\; \{P\} \]

\[ \mbox{nice_program}\;\; P\;\; s \quad\Longrightarrow\quad \mbox{nice_formula}\;\;(\mbox{wip}\;\; P\;\; s) \]

Uniqueness Predicates

fun uve :: "valueExp => bool"
and upe :: "pathExp => bool" where
 
  "uve (Val _)       = True"
| "uve (Var _)       = True"
| "uve (Con _)       = True"
| "uve (Sum _)       = True"  (* always empty *)
| "uve (Size _)      = True"  (* always empty *)
| "uve (Tally _ _)   = True"  (* always empty *)
| "uve (Count _ _)   = True"  (* always empty *)
| "uve (Scal _ m)    = uve m" (* always empty... *)
| "uve (Read _ p)    = upe p"
| "uve (VPlus _ _)   = False" (* not, if not statically discarded *)
| "uve (VRep _ _)    = False" (* uniquely diverse *) (* would be ok, but easy enough to get rid of *)
| "uve (VCond _ t e) = (uve t \<and> uve e)"
 
| "upe PRoot         = True"
| "upe (Path _ p i)  = (upe p \<and> uve i)"
| "upe (Kind _ p)    = False" (* either empty or infinite, but not single, CAN BE EMPTY... *)
| "upe (PRep _ p)    = False" (* uniquely diverse *) (* would be ok, but easy enough to get rid of *)
| "upe (PPlus a b)   = False"
| "upe (Diff a b)    = False"
| "upe (PCond _ t e) = (upe t \<and> upe e)"

¹⁾

I believe I can even transform every formula to get to this property, but that's not the important thing.

PBMichel.de

Table of Contents