proposal: standardize bex notations

[tangentstorm]

There should be a standard syntax for referring to objects in the bex mini-language and string outputs.

Here is one proposal.

nid notation

Note: these should be easily writable in a URL for the HTTP server.

• O and I (letters that look like 0 and 1 are the constant nids for false and true.
• xN, where N is an upper case hex number, is an input variable (ex: x0, xEB)
• vN, where N is an upper case hex number, is a "virtual" variable, generally used to refer to a made-up variable assigned to a node in an AST. Ex: vF3.
• '!xNand!vN` are the same, but represent inverted literals
• tBBB...B is a table nid where each B is either a 0 or 1 (alt: O/I) and there are 2^n of them, where n is between 1 and 5, inclusive. ex: t0001 is the truth table for the dyadic AND function
• fN.MMM....M is the same but in hex (so f2.6 == t0110 ("XOR"), and f3.33
• fN is f2.N
• !xNN.MMMM is a VHL NID at address MMMM in the hilocache. (MMMM is just another hex number). xNN or vNN is the branching variable.
• !xNN.MMMM is the same but inverted
• @MMMM is the NID for the AST node at index MMMM
• !@MMMM is the same, but inverted
• If dealing with multiple bases, a numeric namespace N: can appear as a prefix.

operators

symbol	meaning
pipe	or
&	and
%	xor
=	equal
!	not
<	less than (x < y means "y and not x")
/	less than or equal to (x / y means "x implies y")
?:	if then else ( f ? g : h means "if f then g else h")

(pipe means | but github's markdown won't let me put that character in a table)

Tables can also be used as operators using bracket notation. Ex: t1[x y] is the same as x *. y

The bracket notation can also be used as an an alternate syntax for if/then/else when the f argument is a variable.

If the bracket notation is used on a BDD or AST nid (anything with an index MMMM), that means to substitute the arguments into the corresponding structure, from the "top down". So for example, if you pass two arguments to a BDD branching on x5, you would generally get back the NID for a new BDD branching on x3 (provided the arguments themselves didn't introduce new variables).

(For consistency, the same "top-down" substitution order probably should be applied for AST nodes, although that feels rather backwards to me... Alternatively, we could just disallow this operation for AST nodes until someone actually wants it.)

multiple grammars

The above notations would be used as a common "vocabulary", not a "grammar", because bex isn't meant to be a specific language.

If we want to present a traditional algebraic notation, the above operators could be used in infix form, assigned to
named variables (probably using : as the assignment operator), and nested arbitrarily using parentheses.

OTOH, The bex shell uses a forth-like RPN notation. Nesting could still be allowed using quotations (brackets) but the operators would generally be used postfix. That means instead of f ? g : h we might write f g h ?: ... the point is the "verb" for the if/then/else operator is spelled ?: either way. (In order to apply a NID to arguments in RPN, there would have to be some extra sigil indicating that the nid is meant to be applied rather than simply added to the stack.)

Likewise, the same vocabulary can be used with a JSON grammar for easily exchanging expressions with other programming languages.

JSON notation

Any of the above notations for primitive NIDs can be used directly in a single JSON string. So the JSON for O is just "O".

Compound nodes can be serialized as a dictionary mapping a single operator to a list of arguments. Example: { "+" : ["x0", "x1"]} is "x0 OR x1". As a special case, the ~ operator can elide the list wrapper: {"~": "x3"} (which is the same as "X3")

If you want to apply a NID as a function, the NID can be used as an operator. For example: { "nv5.234" : ["x2", "x93"]} might give back "nv3.122" (which is some other bdd node after replacing "v5" with "x2" and "v4" with "x93" in "nv5.234").

{"?:" ["x9", "nx8.324", "nx4!54C"]} would be an example of constructing / locating a new BDD node directly, by passing a branch VID and two NIDs to the if/then/else operator.

[tangentstorm]

alternate operator notation

I originally wrote the following for the operators:

symbol	meaning
+.	or
*.	and
~:	xor
=	equal
-.	not
<	less than (x < y means "y and not x")
<:	less than or equal to (x <: y means "x implies y")
?:	if then else ( f ? g : h means "if f then g else h")

These are the operators from the J programming language (except ?: which would be something like [email protected]`h).

The thought was that bex has a feature that lets you work with multi-bit structures and perform actual arithmetic on them... So in that case, + should call bex::int::wrapping_add to construct an integer addition circuit.

Overloading is fine, but then what do you use when you want to bitwise OR two of these "integers"?

The other obvious scheme is |, &, and ^ as in C. (I also like #, which Oberon uses for "not-equals" (XOR is bitwise "not-equals")).

This is probably more familiar to python/js devs.

Lean and isabelle (proof assistants) both just use unicode symbols and have latex-based escapes built into the editor modes to type the funny characters.