Examples

The language defining itself, one definition at a time, in the order that dependency demands: the dyad, the ground type, scope, the scope opener (, fn, the operator ^ built out of all of it, and proof. The definitions come from the language's own source files with their comments stripped, in the spellings the design rules today. type and ^ run in the seed; the others are sketches the seed still realises in Rust.

dyad

The one node the Logic Graph is made of: a type and a value. Its type field is itself a dyad, so the first definition already refers to itself.

dyad := type (type := @dyad ?, value := @void ?)

type

The ground: an instance of itself and the definition word. Its body declares, once, the slots every type fills with =, and then fills its own: how its spelling parses, reading its bracket and making its own cell the finished type. Runs in the seed today.

type := type (  parse_rank    := f64 ?,  associativity := ?,  parse         := parse ?,  run           := run ?,  drop          := drop ?,  share parse_rank    = f64 2.0,  share associativity = left,  share parse = (    if tape[1] != lex «(»[0]      error «type must be followed by (»,    tape[0]:type = type,    (.parse(tape.recenter(1)),    tape.is_constructed[0] = true,    tape.remove(1)  ))

scope

A scope is a node that holds its nodes in order, dyads, and the scope it stands in, back, null at the arche. Its parse is still a hole; ( is what fills a scope.

scope := type (  dyads := array dyad [],  back  := @scope ?,  share parse = ( ? ))

(

The scope opener is the driver of the parse. Constructed the moment it is lexed, it reads its interior one cell at a time: a cell that binds at least as tightly as ( is constructed on the spot, and at each , or the closing ) the rest of the segment is constructed highest rank first. The constructed cells, in order, become the scope.

( := type (  share parse_rank    = f64 9.0,  share associativity = left,  share parse = (    body      := array @dyad [],    mut first := 1,    mut i     := 1,    while true (      cell := tape[i],      if cell == lex «)»[0] or cell == lex «,»[0] (        while true (          k := highest_unconstructed(tape, first, i),          if k == ? break,          tape[k].parse(tape.recenter(k))        ),        for k in first..i (          if not tape.is_constructed[k]            error «unconstructed cell at a segment boundary»,          body.push(tape[k])        ),        if cell == lex «)»[0] break,        first = i + 1      ) else if cell.parse_rank >= (.parse_rank (        cell.parse(tape.recenter(i))      ),      i = i + 1    ),    tape[0]:type = scope,    tape[0].dyads = body,    tape.is_constructed[0] = true,    for k in 1..i+1 ( tape.remove(1) )  ))

fn

A function is a type in the same shape as any operator: its parameters are its fields, its declared result its output_type, its body its run, with a call's defaults for where it binds and how it parses. What the sketch declares besides is what the seed's fn carries: the input type, the compiled code and the frame size. compile f lowers the body to machine code, and a call jumps to the code when there is some and walks the body when there is not.

fn := type (  input       := type ?,  output_type := ?,  bcode       := callable ?,  frame       := u64 ?,  share parse_rank    = …,  share associativity = left,  share parse         = ( ? ))

^

An operator built out of all of the above, and the v0.1.0 demo: the language defines itself. Its body says what a ^ node holds, the operands as named fields and the output the parse writes per node; where it binds and which way it associates; what happens when ^ stands on the tape, a parse over the cells around it that makes its own cell the new node; and what every node computes, a run over its fields by name, over integers and floats with any real exponent, exp and ln being ordinary Logos functions in their own files. Runs in the seed today, compiled with compile f.

import ln.logos,import exp.logos,^ := type (  lhs := ?,  rhs := ?,  output_type := type ?,  share parse_rank = *.parse_rank + 1,  share associativity = right,  share parse = (    tape[0]:type = ^,    tape[0].lhs = tape[-1],    tape[0].rhs = tape[1],    if tape[-1]:type == f64 or tape[1]:type == f64 (      tape[0].output_type = f64    ) else if tape[-1]:type == f32 or tape[1]:type == f32 (      tape[0].output_type = f32    ) else if tape[1]:type == rational_number and not (tape[1]:type ⊆ i64) (      tape[0].output_type = f64    ) else (      tape[0].output_type = tape[-1]:type    ),    tape.is_constructed[0] = true,    tape.remove(1),    tape.remove(-1)  ),  share run = (    if (f64(rhs) == f64(i64(rhs))) (      mut power := output_type 1,      mut times := i64(rhs),      mut factor := output_type(lhs),      if times < 0 (        if not (output_type == (f64 or f32 or rational_number))          error «a negative exponent of a whole number is not whole: write the base as a float»,        factor = output_type 1 / factor,        times = 0 - times      ),      for 0..times ( power = power * factor ),      power    ) else if (output_type == (f64 or f32)) (      real_base := f64(lhs),      if real_base < 0.0        error «a negative base has no real power for a fractional exponent»,      if real_base == 0.0        output_type 0      else        output_type (exp(f64(rhs) * ln(real_base)))    ) else      error «a fractional exponent needs a float result»  )),f := fn (x := i32 ?) -> i32 ( x ^ 3 + 1 ),compile f,f(2)   # 9

proof

A proof is a rewrite rule together with its evidence: the holes it quantifies over, the premises that must hold, a pattern and its replacement, the derivation from one to the other, and the world of axioms it rests on. Its parse is still a hole.

proof := type (  holes       := array dyad [],  premises    := array dyad [],  pattern     := dyad ?,  replacement := dyad ?,  derivation  := ?,  world       := array @proof [],  share parse = ( ? ))