48 Proofs about syntax — whichever closer closes it, the same tree

48.1 Algebra and denotation#

Joining statements has two properties. The way they join does not depend on grouping (associativity), and an empty block is nothing (identity — what 0 does for addition). A structure with both is a monoid. Concatenating lists is the typical monoid, and a program’s sequence of statements has exactly that structure.

To say whether two spellings are “the same” you need a criterion. Take a function denote sending each tree to a flat sequence of statements, and call them the same if the results match. denote(do S end) = [S] = denote(S), so the two are the same. This is the only technique in this chapter — define “the same” by a function and confirm equations by computation.

48.2 One statement is a one-statement block#

module oneform .
rem run: bare 3
rem run: blocked 3
rem fmt

fn bare input a u64 . output u64 .
  requires le a 1000 .
do
  var x u64 be a .
  if gt a 1 . set x (add x 10) .
  return x .
end

fn blocked input a u64 . output u64 .
  requires le a 1000 .
do
  var x u64 be a .
  if gt a 1 . do
    set x (add x 10) .
  end
  return x .
end

$ lowentc --run bare oneform.low 3
bare(3) = 13
$ lowentc --run blocked oneform.low 3
blocked(3) = 13
$ lowentc --fmt oneform.low
module oneform .
fn bare .
  input a u64 .
  output u64 .
  requires le a 1000 .
do
  var x u64 be a .
  if (gt a 1) do set x (add x 10) . end
  return x .
end
fn blocked .
  input a u64 .
  output u64 .
  requires le a 1000 .
do
  var x u64 be a .
  if (gt a 1) do set x (add x 10) . end
  return x .
end

bare writes one statement directly as the body of if, and blocked wraps it in do … end. The answers are the same, and the canonical form printed by --fmt does not differ by a single character.

This theorem justifies a design decision. C separates statements and compound statements into different kinds. if (c) x = 1; and if (c) { x = 1; } are grammatically different, and the famous goto fail; trap came from that gap — the indentation made two lines look as if they belonged to the if, but the grammar made only one belong. Lowent does not separate them.

 C       if (c)
             x = x + 10;
             y = 0;          ← indented as if inside the if, but the grammar puts it outside

 Lowent  if gt a 1 . set x (add x 10) .        one statement = a one-statement block (G1)
         if gt a 1 . do
           set x (add x 10) .
           set y 0 .
         end                                   a longer body is ended by end

48.3 Closers do the same job#

Seen in an example:

module closers .
rem run: one_line 4
rem run: spread 4

fn one_line input x u64 . output u64 .
  requires le x 1000 .
do
  return add (mul x x) (add x 1) .
end

rem spreading arguments over several lines needs no marker --- a newline is whitespace
fn spread input x u64 . output u64 .
  requires le x 1000 .
do
  return add
    (mul x x)
    (add x
         1) .
end

$ lowentc --run one_line closers.low 4
one_line(4) = 21
$ lowentc --run spread closers.low 4
spread(4) = 21

In one_line the two ) close the inner forms and . closes the outer one. spread lays the same form over four lines with no marks needed, because a newline is whitespace. Both ops give the same answer.

 return add (mul x x) (add x 1) .      return add
                                           (mul x x)
                                           (add x
                                                1) .
 both become the same tree:
                 add
            ┌─────┴─────┐
           mul         add
          ┌─┴─┐       ┌─┴─┐
          x   x       x   1

A newline could also be made a closer, and that is provable too. It still is not done. If newlines closed, line breaks would carry meaning, and merely splitting a long line would change the program. That a meaning can be proven the same does not mean the spelling must exist. Theorems once attached to commas, line continuation and newline closing were all Qed too, but when those rules left the language, the theorems left with them. Today , and ; are rejected with E-VOCAB-REMOVED — a word that parses but has no effect is a silent trap. Keeping theorems modelling dead rules would make a proven document speak of rules that do not exist.

Every proof in this file ends by computation. The value is not in the difficulty of the proofs but in having chosen and written the propositions. With “closers do the same job” written down, the proof breaks when someone treats one specially. Syntax is a layer that quietly drifts with “it would be convenient to make an exception just here”, and theorems catch that drift. What they stop are not users’ defects but the compiler’s.

48.4 Common mistakes#

module mistake_noperiod .
rem expect: E-IR-ARITY

fn total input a u64 . input b u64 . output u64 .
  requires le a 1000 .
  requires le b 1000 .
do
  rem ✘ the period at the end of this line is missing
  var s u64 be add a b
  set s (mul s 2) .
  return s .
end

$ lowentc --check mistake_noperiod.low
mistake_noperiod.low:10:0 E-IR-ARITY: extra operands in expression (strict arity)

module mistake_semicolon .
rem expect: E-VOCAB-REMOVED
fn twice input a u64 . output u64 .
  requires le a 1000 .
do
  rem ✘ closing with a semicolon, as in C
  return mul a 2 . ;
end

$ lowentc --check mistake_semicolon.low
7:20 E-VOCAB-REMOVED: `;` was a THIRD spelling of the closer `.` (the lexer literally emitted a DOT for it) — one meaning, three spellings, and SPEC-002 §2.5 forbids synonyms. It only survived inside the old interpreter's second language. Write `.`

48.5 What is not proven#

• There is no guarantee that the real parser is this model. The model is a few small functions building trees, and the real parser is much larger. The correspondence is backed by unit and regression tests.
• denote is a flat sequence. Position information, comments and error recovery were not modelled. So “the same tree” means the same structure, not the same diagnostic quality.
• The lexical (token) layer is separate. Whether tokens split exactly into this model’s three closers is the lexer tests’ job.