## Operational Semantics

Computation within MM2 takes place via the `exec` construct that has the following structure

```scheme
(exec SYSTEM PATTERNS TEMPLATES)
```

- `SYSTEM` can be currently understood as a priority (see further details below).
- `PATTERNS` is a comma separated collection of patterns that must be matched.
- `TEMPLATES` is a comma separated collection of rewriting templates that will be written to the global space.

It looks like the computational loop works as follows: 
1. At each step select the `exec` instruction with the highest priority.
2. Pattern match the conjunction of patterns in `PATTERNS`.
3. Write the content of the templates to the global space.
4. Consume the `exec` instruction (remove it from the global space).

Note that the `exec` instruction is consumed no matter what, regardless of whether any pattern matched.

### Priority Ranking of the System Argument

Among possibly other usages `SYSTEM` is used to determining the priority of selecting `exec` among a multitude.  An empirical search seems to indicate that priority is set according to the following rules, form an expression-preferring [shortlex](https://en.wikipedia.org/wiki/Shortlex_order)-like ordering:

- Expression has higher priority than symbol. For instance `(exec (d e f) ...)` is selected over `(exec a ...)`.
- If both are expressions, then the lower arity expression has higher priority. For instance `(exec (a b) ...)` is selected over `(exec (d e f) ...)`.
- If both are symbol, then shorter symbol has higher priority. For instance `(exec z ...)` will be selected over `(exec ab ...)`.
- If both are symbols of equal size, then symbol coming earlier in lexicographic order has higher priority. For instance `(exec abc ...)` will be selected over `(exec abz ...)`.
- Individual characters are ordered according to [ASCII codes](https://www.ascii-code.com/).  For instance `(exec 1 ...)` is selected over `(exec A ...)` which is selected over `(exec a ...)`.
- If all priorities are equal, then MM2 will pick up one of them according to some arbitrary (but not random) order determined by the content of `exec` instructions.

### Syntax Basics

1. Comments are denoted by ; as in [MeTTA HE](https://github.com/trueagi-io/hyperon-experimental).

### Querying Spaces from Rust

A _Space_ in Rust can be queried with the _dump_sexpr(pattern, template, output)_ and _dump_all_sexpr(output)_ functions.

The [N] notation in queries specifies traversal depth in the tree structure.

For example, the following code will query Space _s_ for the proof to the statement that "|- t = t". The instruction is that _ev_, _:_, and _⟨=⟩_ all have three arguments (including themselves) if there is a proof to extract with $ and ev has two arguments if there is no proof.  The variables are extracted by De Bruijn indexes denoting their order of appearance.

```rust
let mut q_proof = Vec::new();
s.dump_sexpr(
    expr!(s, "[3] ev [3] : [3] ⟨=⟩ ⟨t⟩ ⟨t⟩ ⟨|-⟩ $"),
    if with_proof {
        expr!(s, "[3] ev [3] : [3] ⟨=⟩ ⟨t⟩ ⟨t⟩ ⟨|-⟩ _1")
    } else {
        expr!(s, "[2] ev [3] : [3] ⟨=⟩ ⟨t⟩ ⟨t⟩ ⟨|-⟩")
    },
    &mut q_proof
);
```

Output: `(ev (: (⟨=⟩ ⟨t⟩ ⟨t⟩) ⟨|-⟩) (⟨mp⟩ (⟨a2⟩ ⟨t⟩) (⟨mp⟩ (⟨a2⟩ ⟨t⟩) (⟨a1⟩ (⟨tpl⟩ ⟨t⟩ ⟨0⟩) ⟨t⟩ ⟨t⟩))))`

### Function Application

There is no built-in function application, so it needs to be implemented via pattern matching.

Input MM2:
- `(kb (: ⟨a2⟩ (-> (: $a ⟨term⟩) (: (⟨=⟩ (⟨+⟩ $a ⟨0⟩) $a) ⟨|-⟩))))`
- `(kb (: ⟨t⟩ ⟨term⟩))`

Whereas the following works:
```lisp
(exec (4 app1)
  (, (ev (: $name (-> $a $b)))
     (ev $a))
  (, (ev $b)
     (applied ($name $a) to get $b)))
```

Result:
- `(ev (: (⟨=⟩ (⟨+⟩ ⟨t⟩ ⟨0⟩) ⟨t⟩) ⟨|-⟩))`
- `(applied (⟨a2⟩ (: ⟨t⟩ ⟨term⟩)) to get (: (⟨=⟩ (⟨+⟩ ⟨t⟩ ⟨0⟩) ⟨t⟩) ⟨|-⟩))`

### Backend (where the MM2 code lives)

This is rust, but it's the canonical source with respect to understanding behavior:

1. Inside the file https://github.com/trueagi-io/MORK/blob/main/kernel/src/main.rs any constructor (const) or function (fn) with mm2 in the name is relevant. There are also a number of comments containing the string `MM2` which could possibly be helpful.

2. Also, there's one other file with 2 relevant functions. As of 2025.09.25, they are located just below https://github.com/trueagi-io/MORK/blob/728e83e3d396ed409be0124167034b43652d68e6/kernel/src/space.rs#L1306 extending to line 1357 -- in case modifications are made to shift those line numbers, the 2 functions are: `pub fn interpret(&mut self, rt: Expr)` and `pub fn metta_calculus(&mut self, steps: usize) -> usize`.

### Mappings into MeTTa
There's only one statement (with 4 variations)
`(exec <sys> (, <patterns>) (, <templates>))`
which maps to
`(match &<sys>  (, <patterns>) (superpose (add-atom &self <templates>) ))` in MeTTa

For one of the variations (sinks)
`(exec <sys> (, <patterns>) (O (+ <pos>) (- <neg>) <others>))`
is the same as 
```
(match &<sys>  (, <patterns>) (add-atom &self <pos>))
(match &<sys>  (, <patterns>) (remove-atom &self <neg>))
```

### Improving runtime
Order your conjunctives to minimize iteration.
```
; bad: 
(exec <sys> (, (mul $x $y) (input $x)) (, (output $y)))
; good
(exec <sys> (, (input $x) (mul $x $y)) (, (output $y)))

; bad (runtime |A $|^2 * |A _ $|^2 * |parity <i> $| ):
((phase $p)  (, (A $i $e) (A $si $se) (parity $i $p) (succ $i $si) (lt $se $e))
             (O (- (A $i $e)) (- (A $si $se)) (+ (A $i $se)) (+ (A $si $e))))
; good (runtime |parity $| * |parity <i> $| * |succ <i> $| * |A <i> $| * |A <si> $| ):
((phase $p)  (, (parity $i $p) (succ $i $si) (A $i $e) (A $si $se) (lt $se $e))
             (O (- (A $i $e)) (- (A $si $se)) (+ (A $i $se)) (+ (A $si $e))))
```

Split up disjoint operations in your conjunctive.
```
; bad:
(exec <sys> (, (Bar ($i $x)) (Baz ($j $y))) (, (Foo ($i $x)) (Foo ($j $y))))
; good:
(exec <sys_1> (, (Bar ($i $x))) (, (Foo ($i $x))))
(exec <sys_1> (, (Baz ($j $y))) (, (Foo ($j $y))))
```