Up

scalars

scalar types include at least integers, with the usual operations (+), (*), (-), (/), (%), with the latter two integer division and remainder; and bytestrings, where "food"*"foobar"=="foo" and "foo"/"bar" == "foobar".

bunches

compound bunches are constructed with (|), but note that elemental bunches (and the degenerate bunch: Null) are also considered to be bunches.

bunches are unordered collections which ignore repetition.

NB. it is expected that bunches are mostly used for specification and to indicate possible parallelisation; most implementation code will be in terms of elements (see later: continuity of application)

x|x == x
x|y == y|x
x|(y|z) == (x|y)|z
Null | x == x

bunches have a natural ordering relation (~)

x~y := x|y == y

x~x
x~y && y~z ==> x~z
x~y && y~x <=> x == y
Null ~ x ~ (x|y)

Exercise: prove Null~x

the dual operation to (|) is (&)

z~x && z~y && (a~x && a~y ==> a~z) <=> x&y == z

x&x == x
x&y == y&x
x&(y&z) == (x&y)&z
Nuts & x == x
Null ~ (x&y) ~ x ~ (x|y) ~ Nuts

x & (y | z) == x&y | x&z
x | (y & z) == (x|y)&(x|z)
x  & y | y == y
(x | y) & y == y

x~y ==> (x&z) ~ (y&z)
x~y ==> (x|z) ~ (y|z)

(x|y)~z == x~z && y~z
x~(y|z) == x~y || x~z     NB. x element

sequences

complex sequences are constructed with (,), but note that simple length-1 sequences (items), and the degenerate length-0 sequence Nil, are also considered to be sequences.

sequences are ordered collections which preserve repetition; they are also elements.

OPEN: might it be better to use (;) for sequences and allow (,) as sugar to denote either (;) or (|) depending upon context of closest enclosing brackets?

x <> y := not (x == y)

Nil, x == x == x, Nil
proper x ==> x, x <> x
x, (y, z) == (x, y), z

x, (y | z) == x, y | x, z
(x | y), z == x, z | y, z

Star x == Nil | x | Star x, Star x

s \lexle s, t
Nil \lexle s
s \lexle s

i <= j <=> u, i, v \lexle u, j, w

Exercise: prove x, Null == Null == Null, x

lists

lists package sequences, and hence are simple items.

[x] ::= List x

[x|y] == [x]|[y]
x <> Null ==> [x] <> x
[s] <= [t] <=> s \lexle t

indexing of lists

	[i, j, k].1 == j
        [i, [j, k], l].(1,0) == j
        [i, [j, k], l]%?(1,0) == [j,k],i

in addition, [i, j, k]*[i, l, m] == [i] and [i, j]/[k, l] == [i, j, k, l]

sets

sets package bunches, and hence are elements (as well as items)

{x} ::= Set x

{x} <> x
{x|y} <> {x}|{y}

{x} <= {y} := x ~ y

todo: total order, partial order

sets have intersection (*), xor (+), eqv (-), and union (%).

row ::= key: value

for technical reasons, rows have an "upside-down" ordering and hence skew-distribute over bunch formation

k: (v|w) <> (k: v) | (k: w)

footnote: Null <= (k: (v|w)) <= (k: v) <= (j&k: v) <= Nuts

when packaged in sets, rows produce finite maps (see next page)

example

{ subject	: Socrates
| category	: [substance, mortal, animal, primate, man]
| affection	: poisoned }	NB. ontology ca. 300 BC

Next