Compute space (cspace) is the subset of gspace which defines basic computation and universal statements (proofs).
A name is in cspace if and only if it is a pair whose head is blank.
Almost all names in cspace are constrained by this spec (the cspec). A few are reserved. It seems unlikely that any future cspec will bind the reserved names, but it's not impossible.
The cspec is written in a simple pattern-matching notation. Nothing parses this notation. It is just here for clarity.
The cspec notation has the following grammar:
cspec: *cpart
cpart: cdeclare | cgroup
cdeclare: '*' '(' cpattern ')' ':' (cvalue | ctext)
cgroup: '*' '(' cpattern ')' '{' *cpart '}'
ctext: '<<' *[a-zA-Z \n] '>>'
cpattern: clwildcard | cblank | cinteger | '(' +cpattern ')'
cvalue: crwildcard | cblank | cinteger | '(' +cvalue ')'
clwildcard: '$' ?cshape *[a-z]
crwildcard: '$' *[a-z]
cshape: +ctest
ctest: '.' | '_' | '~' | '%'
cblank: '.' | '_' | '~'
cinteger: '.' +[0-9]
A declaration is just a name-value binding with wildcards. A wildcard can match any detail, or be restricted by shape. Declarations can also be grouped for readability.
In wildcard shape tests, '.' means a blank, '_' means an
integer, '|' means a blank which is not qi, and '~' means a pair.
A wildcard with multiple tests may match any; for example,
$._wild matches any blank or integer.
Any name in cspace which does not match a declaration in this space is reserved. Reserved names may be bound by future cspecs. Declarations do not overlap: no detail matches more than one pattern.
This notation is not powerful enough to express the whole cspec formally. Therefore, some values are defined using normative text enclosed in double angle brackets.
;- Gvalue of a pair headed by qi: identity space.
;-
*(~ $itself):
$itself
;- Gvalue of a pair headed by yin: mix space.
;-
;- A mix is a simple expression expansion, with recursion
;- and computational axioms to make it Turing-complete.
;-
*(. $mix) {
;- The mix of a blank or integer is itself. Rarely used.
;-
*(. $._flat):
$flat
;- A nontrivial mix is an expression-argument pair.
;-
*(. $expression $argument) {
;- The simplest expression (and probably the most common)
;- is just a blank or integer.
;-
*(. $._flat $argument):
$flat
;- Unless the head of a pair expression is qi, its mix is
;- just the pair of left and right mixes.
;-
*(. ($|_~left $right) $argument):
(*(. $left $argument) *(. $right $argument))
;- When the head of a pair expression is qi, it is a control
;- expression with special semantics.
;-
;- In other words, ~ is basically an escape code.
;-
*(. (~ $control) $argument) {
;-
;- Normal control patterns: basic structure.
;-
;- Reference the argument.
;-
*(. (~ ~) $argument):
$argument
;- Include quoted text.
;-
*(. (~ _ $quote) $argument):
$quote
;- Dereference in G.
;-
*(. (~ . $remix) $argument):
*(*(. $remix $argument))
;- Normal control patterns: computational axioms.
;-
;- This may not be the smallest possible set, but
;- hopefully it is the most straightforward.
;-
;- Note that all remaining patterns within the space
;- *(. (~ .) $argument), and all patterns within the space
;- *(. (~ _) $argument), are reserved in this version.
;-
;- Axiom 0: shape.
;-
*(. (~ .) (%0 $.blank)): .
*(. (~ .) (%0 $~pair)): ~
*(. (~ .) (%0 $_integer)): _
;- Axiom 1: if.
;-
*(. (~ .) (%1 . $sic $non)): $sic
*(. (~ .) (%1 _ $sic $non)): $non
;- Axiom 2: blank equality.
;-
*(. (~ .) (%2 . .)): .
*(. (~ .) (%2 . ~)): _
*(. (~ .) (%2 . _)): _
*(. (~ .) (%2 ~ .)): _
*(. (~ .) (%2 ~ ~)): .
*(. (~ .) (%2 ~ _)): _
*(. (~ .) (%2 _ .)): _
*(. (~ .) (%2 _ ~)): _
*(. (~ .) (%2 _ _)): .
;- Axiom 3: integer addition.
;-
*(. (~ .) (%3 $_this $_that)):
<<
The integer sum of $this and $that.
>>
;- Axiom 4: integer negation.
;-
*(. (~ .) (%4 $_integer)):
<<
The product of $integer and -1.
>>
;- Axiom 5: integer sign.
;-
*(. (~ .) (%5 $_integer)):
<<
., ~, or _ if $integer is less than,
equal to, or greater than 0 respectively.
>>
;- Secondary control patterns. Every expression which
;- uses secondary patterns directly has an equivalent
;- which does not. (In other words, these patterns
;- add no formal computational power to G.)
;-
;- Annotation.
;-
;- There are three kinds of annotation: debug or
;- trace information, computational hinting, or
;- anything else (private information). Patterns
;- for the first two are higher-level standards.
;-
;- Note that names not matching the hint, trace,
;- or private patterns remain reserved.
;-
*(. (~ ~ $._flat) $argument):
$flat
*(. (~ ~ $note $notable) $argument) {
*(. (~ ~ (. $hint) $notable) $argument):
*(. $notable $argument)
*(. (~ ~ (_ $trace) $notable) $argument):
*(. $notable $argument)
*(. (~ ~ (~ $private) $notable) $argument):
*(. $notable $argument)
}
;- Shorthands. These are just simple ways of
;- representing common operations with unused
;- detail bandwidth.
;-
;- When writing program transformation code, never,
;- ever, ever check for shorthands directly. Always
;- convert to the equivalent normal expression first.
;-
;- Use an expression by name.
;-
*(. (~ $_~operator $operand) $argument):
*(. *($operator) *(. $operand $argument))
;- Reference a named variable, using a style
;- in which the argument is itself an expression
;- which resolves the variable name.
;-
*(. (~ $_variable) $argument):
*(. $argument $variable)
}
}
}
;- Gvalue of a pair headed by yang: universal space.
;-
;- A universal statement generalizes across an infinite set of
;- mix results. To resolve a value in universal space is to
;- prove the statement.
;-
;- When $tvalue is ., the ustatement is called a _proposition_.
;- All statements can be normalized as propositions.
;-
*(_ $._flat): .
*(_ $tname $tvalue):
<<
. if for every $argument:
**(. $tname $argument) = *(. $tvalue $argument)
_ otherwise, except
~ if the value of *(_ $tname $tvalue) would affect
the definition of **(. $tname $argument) or
*(. $tvalue $argument).
>>