loa

Virtual machine for the Logic of Assumptions
git clone git://juanmeleiro.mat.br/loa
Log | Files | Refs

NOTES.md (1726B)


      1 - AllwoodZipper2010
      2 
      3 # Model
      4 
      5 The state of the machine consists of the following:
      6 
      7 - `cursor`: the structure built so far. Starts as `empty`.
      8 - A `focus`: if there at least one hole in the structure, a pointer to the first one.
      9 
     10 All data structures can have child values replaced with a *hole*, which
     11 has a type corresponding to the shape of what can fill that hole. When
     12 focused on a hole with a certain type, the machine expects the next
     13 instruction to indicate a constructor of that type. For example:
     14 
     15 - If the hole is for a **number**, it expects a number.
     16 - If the hole is for a **symbol**, it expects a symbol.
     17 - If the hole if for a list, it expects **empty** or **cons**.
     18 
     19 When meeting such an instruction, the machine will then *fill* the hole
     20 with a *template* for that constructor. That just means it will put a
     21 value in the hole using that constructor, but with its arguments being
     22 holes of the appropriate types.
     23 
     24 The possible types for holes are those that have more than one
     25 constructor, as all others can be filled automatically. So, that means these:
     26 
     27 - Number
     28 - Symbol
     29 - Lists
     30 
     31 When there is no hole in the structure at the `cursor`, the available
     32 instructions are those that apply constructors using the current structure
     33 as an argument. This means a single one: `top`.
     34 
     35 ```
     36 	top := (attitude | assumption) * top | empty
     37 ```
     38 
     39 So the machine will create a new `top` with the one at `cursor` as its
     40 argument, and a hole for the other argument.
     41 
     42 Finally, when a hole is filled with an atomic value (i.e., there's no
     43 subhole), the `focus` goes to the next available hole.
     44 
     45 Every node in the structure must be verified for its legality conditions
     46 as soon as possible; i.e., as soon as all its holes are filled.