💾 Archived View for oortcloud.flounder.online › junk › 0data.gmi captured on 2024-02-05 at 09:22:38. Gemini links have been rewritten to link to archived content
-=-=-=-=-=-=-
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".
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
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 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 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)
{ subject : Socrates
| category : [substance, mortal, animal, primate, man]
| affection : poisoned } NB. ontology ca. 300 BC