Programs in a rose tree machine (RTM)

This file contains the main definition of the rose tree machine, its programs including semantics and time and space resource consumption.

Main definitions and notations

• Prog - the program
• ProgSem - semantics and resource consumption
• InPlace - a fragment of the language that can be easily simulated using multi-tape Turing machines.
• Prog.ComputesInTimeAndSpace - this defines the complexity notion for the RTM computation model, based on Data values.
• Prog.ComputesBoolFunInTimeAndSpace - the complexity notion transferred to functions on binary strings, this making it compatible to all other computation models.
• ComputableInOTime - generic time-complexity in the RTM model
• ComputableInOSpace - generic space-complexity in the RTM model

@[reducible, inline]

abbrev Complexity.RoseTreeMachine.TapeIndex : Type

Index of a tape cell used by the rose tree machine's execution model.

Equations

• Complexity.RoseTreeMachine.TapeIndex = ℕ

inductive Complexity.RoseTreeMachine.Prog : Type

Prog is the syntax representation of a functional language that has a resource consumption model which is compatible to that of a Turing machine. The data structure it operates on is a rose tree (Data). The advantage of this data structure is that the majority of lean data types have a direct encoding.

• var (id : ℕ) : Prog

  Variable reference at de Bruijn level id.

• empty : Prog

  The empty constructor of Data.

• cons (h t : Prog) : Prog

  The cons constructor of Data: prepend the value of h to the list value of t.

• elim (v emp cs : Prog) : Prog

  Destructor of Data: evaluate v; if it is empty, run emp; otherwise destructure into head and tail and apply the function cs to head and then to tail.

• ifEq (x y then_ else_ : Prog) : Prog

  Equality comparison: If x evaluates to the same data as y, run then_, else run else_. This can be simulated using while_ below, but it is useful to have.

• while_ (init body : Prog) : Prog

  While loop: evaluate init to the starting accumulator; body must evaluate to a one-argument function which is applied to the current accumulator on each iteration. Return the accumulator if its head is empty.

• fn (body : Prog) : Prog

  Abstraction / closure in one variable.

• app (fn arg : Prog) : Prog

  Function application.

@[implicit_reducible]

instance Complexity.RoseTreeMachine.instReprProg : Repr Prog

Equations

• Complexity.RoseTreeMachine.instReprProg = { reprPrec := Complexity.RoseTreeMachine.instReprProg.repr }

def Complexity.RoseTreeMachine.instReprProg.repr : Prog → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

inductive Complexity.RoseTreeMachine.Value : Type

Runtime values for the semantics predicate ProgSem.

• data (d : Data) : Value
• closure (body : Prog) (env : List Value) : Value

@[implicit_reducible]

instance Complexity.RoseTreeMachine.instReprValue : Repr Value

Equations

• Complexity.RoseTreeMachine.instReprValue = { reprPrec := Complexity.RoseTreeMachine.instReprValue.repr }

partial def Complexity.RoseTreeMachine.instReprValue.repr : Value → ℕ → Std.Format

@[reducible, inline]

abbrev Complexity.RoseTreeMachine.Value.empty : Value

The empty Value, wrapping the empty Data node.

Equations

• Complexity.RoseTreeMachine.Value.empty = Complexity.RoseTreeMachine.Value.data (Complexity.Data.l [])

def Complexity.RoseTreeMachine.Prog.hasVar (i : ℕ) : Prog → Bool

Whether the program Prog refers to the variable at de Bruijn index i.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.RoseTreeMachine.Prog.hasVar i (Complexity.RoseTreeMachine.Prog.var j) = decide (i = j)
• Complexity.RoseTreeMachine.Prog.hasVar i Complexity.RoseTreeMachine.Prog.empty = false
• Complexity.RoseTreeMachine.Prog.hasVar i (h.cons t) = (Complexity.RoseTreeMachine.Prog.hasVar i h || Complexity.RoseTreeMachine.Prog.hasVar i t)
• Complexity.RoseTreeMachine.Prog.hasVar i (init.while_ body) = (Complexity.RoseTreeMachine.Prog.hasVar i init || Complexity.RoseTreeMachine.Prog.hasVar i body)
• Complexity.RoseTreeMachine.Prog.hasVar i body.fn = Complexity.RoseTreeMachine.Prog.hasVar i body
• Complexity.RoseTreeMachine.Prog.hasVar i (f.app arg) = (Complexity.RoseTreeMachine.Prog.hasVar i f || Complexity.RoseTreeMachine.Prog.hasVar i arg)

@[irreducible]

def Complexity.RoseTreeMachine.closureSize (body : Prog) (env : List Value) : ℕ

The size of a closure's environment, restricted to variables that body actually references.

Equations

• Complexity.RoseTreeMachine.closureSize body env = Complexity.RoseTreeMachine.closureSize.go body 0 env

@[irreducible]

def Complexity.RoseTreeMachine.closureSize.go (body : Prog) (depth : ℕ) (env : List Value) : ℕ

Equations

• One or more equations did not get rendered due to their size.
• Complexity.RoseTreeMachine.closureSize.go body depth [] = 0

@[irreducible]

def Complexity.RoseTreeMachine.Value.size : Value → ℕ

The size of a Value. The size of data is the length of its encoding and the size of a closure is the sum of the sizes of the referenced variables.

Equations

• (Complexity.RoseTreeMachine.Value.data d).size = d.size
• (Complexity.RoseTreeMachine.Value.closure p env).size = Complexity.RoseTreeMachine.closureSize p env

@[simp]

theorem Complexity.RoseTreeMachine.closureSize_of_noVar {body : Prog} {env : List Value} (h : ∀ (i : ℕ), ¬Prog.hasVar i body = true) : closureSize body env = 0

@[simp]

theorem Complexity.RoseTreeMachine.closureSize_of_var {i : ℕ} {env : List Value} : closureSize (Prog.var i) env = (Option.map (fun (v : Value) => v.size) env[i]?).getD 0

theorem Complexity.RoseTreeMachine.Value.size_data {d : Data} : (data d).size = d.size

theorem Complexity.RoseTreeMachine.closureSize.go_append (body : Prog) (depth : ℕ) (l1 l2 : List Value) : go body depth (l1 ++ l2) = go body depth l1 + go body (depth + l1.length) l2

Splitting the environment of a closure size computation across an append.

theorem Complexity.RoseTreeMachine.closureSize_append (body : Prog) (l1 l2 : List Value) : closureSize body (l1 ++ l2) = closureSize body l1 + closureSize.go body l1.length l2

The closure size over an appended environment splits into the size over the prefix plus the contribution of the suffix (counted starting at depth l1.length).

theorem Complexity.RoseTreeMachine.closureSize.go_mono {body1 body2 : Prog} (env : List Value) (h : ∀ (i : ℕ), Prog.hasVar i body1 = true → Prog.hasVar i body2 = true) (depth : ℕ) : go body1 depth env ≤ go body2 depth env

closureSize.go is monotone in the set of accessed variables.

theorem Complexity.RoseTreeMachine.closureSize_mono {body1 body2 : Prog} (env : List Value) (h : ∀ (i : ℕ), Prog.hasVar i body1 = true → Prog.hasVar i body2 = true) : closureSize body1 env ≤ closureSize body2 env

If every variable accessed by body1 is also accessed by body2, then body1 has a smaller closure size over any environment.

theorem Complexity.RoseTreeMachine.closureSize.go_le_sum (body : Prog) (depth : ℕ) (env : List Value) : go body depth env ≤ (List.map Value.size env).sum

The closure size is bounded by the total size of the environment.

inductive Complexity.RoseTreeMachine.ProgSem : List Value → Prog → Value → ℕ → ℕ → Prop

Semantics of Prog including time and space resource bounds. ProgSem σ p x t s means that on environment σ, the program p evaluates to the value x and uses t time and s space.

• var {σ : List Value} {i : ℕ} : ProgSem σ (Prog.var i) (σ[i]?.getD Value.empty) (σ[i]?.getD Value.empty).size (σ[i]?.getD Value.empty).size
• empty {σ : List Value} : ProgSem σ Prog.empty Value.empty 2 2
• cons {σ : List Value} {head : Prog} {hd : Data} {hd_t hd_s : ℕ} {tail : Prog} {tl : Data} {tl_t tl_s : ℕ} (h₁ : ProgSem σ head (Value.data hd) hd_t hd_s) (h₂ : ProgSem σ tail (Value.data tl) tl_t tl_s) : ProgSem σ (head.cons tail) (Value.data (Data.l (hd :: tl.asList))) (hd_t + tl_t) (hd_s + tl_s)
• elim_nil {σ : List Value} {val : Prog} {t_v s_v : ℕ} {emp : Prog} {r : Value} {t_emp s_emp : ℕ} {cs : Prog} (h₁ : ProgSem σ val (Value.data (Data.l [])) t_v s_v) (h₂ : ProgSem σ emp r t_emp s_emp) : ProgSem σ (val.elim emp cs) r (t_v + t_emp) (s_v + s_emp)

  elim, empty branch: v is the empty list, so run emp in the current environment.

• elim_cons {σ : List Value} {val : Prog} {hd : Data} {tl : List Data} {t_v s_v : ℕ} {cs : Prog} {cv : Value} {t_cs s_cs : ℕ} {cv' : Value} {t₁ s₁ : ℕ} {r : Value} {t₂ s₂ : ℕ} {emp : Prog} (h_v : ProgSem σ val (Value.data (Data.l (hd :: tl))) t_v s_v) (h_cs : ProgSem σ cs cv t_cs s_cs) (h_app₁ : AppSem cv (Value.data hd) cv' t₁ s₁) (h_app₂ : AppSem cv' (Value.data (Data.l tl)) r t₂ s₂) : ProgSem σ (val.elim emp cs) r (t_v + t_cs + t₁ + t₂) (s_v + s_cs + s₁ + s₂)

  elim, cons branch: v destructures to hd :: tl; evaluate the function cs to a closure and apply it first to hd and then to tl (so cs is a curried two-argument function).

• ifEq_then {σ : List Value} {x : Prog} {vx : Data} {t_x s_x : ℕ} {y : Prog} {t_y s_y : ℕ} {then_ : Prog} {r : Value} {t_then s_then : ℕ} {else_ : Prog} (h_x : ProgSem σ x (Value.data vx) t_x s_x) (h_y : ProgSem σ y (Value.data vx) t_y s_y) (h_then : ProgSem σ then_ r t_then s_then) : ProgSem σ (x.ifEq y then_ else_) r (t_x + t_y + t_then) (s_x + s_y + s_then)
• ifEq_else {σ : List Value} {x : Prog} {vx : Data} {t_x s_x : ℕ} {y : Prog} {vy : Data} {t_y s_y : ℕ} {else_ : Prog} {r : Value} {t_else s_else : ℕ} {then_ : Prog} (h_x : ProgSem σ x (Value.data vx) t_x s_x) (h_y : ProgSem σ y (Value.data vy) t_y s_y) (h_neq : vx ≠ vy) (h_else : ProgSem σ else_ r t_else s_else) : ProgSem σ (x.ifEq y then_ else_) r (t_x + t_y + t_else) (s_x + s_y + s_else)
• while_ {σ : List Value} {init : Prog} {acc : Data} {t_init s_init : ℕ} {body : Prog} {bodyVal : Value} {t_body s_body : ℕ} {r : Data} {t_w s_w : ℕ} (h_init : ProgSem σ init (Value.data acc) t_init s_init) (h_body : ProgSem σ body bodyVal t_body s_body) (h_while : WhileSem bodyVal acc r t_w s_w) : ProgSem σ (init.while_ body) (Value.data r) (t_init + t_body + t_w) (s_init + s_body + s_w)

  while_ init body: evaluate init to the starting accumulator and body to a one-argument closure, then iterate the closure via WhileSem until it halts.

• fn {σ : List Value} {body : Prog} : ProgSem σ body.fn (Value.closure body σ) (Value.closure body σ).size (Value.closure body σ).size

  fn body: evaluate to a closure capturing the current environment σ. The cost is the size of the resulting closure (mirroring var, which charges the size of the value it produces).

• app {σ : List Value} {fn : Prog} {fv : Value} {t_f s_f : ℕ} {arg : Prog} {v : Value} {t_a s_a : ℕ} {r : Value} {t_b s_b : ℕ} (h_fn : ProgSem σ fn fv t_f s_f) (h_arg : ProgSem σ arg v t_a s_a) (h_app : AppSem fv v r t_b s_b) : ProgSem σ (fn.app arg) r (t_f + t_a + t_b) (s_f + s_a + s_b)

  app fn arg: evaluate fn to a closure, evaluate arg to a value, then run the closure's body in the captured environment extended with the argument (static scoping).

inductive Complexity.RoseTreeMachine.AppSem : Value → Value → Value → ℕ → ℕ → Prop

Application of a value to an argument value. AppSem f v r t s means that applying the closure f to the argument v yields r using t time and s space. Only closures can be applied; applying a first-order value has no derivation (the program is stuck).

• mk {σ : List Value} {v : Value} {body : Prog} {r : Value} {t s : ℕ} (h_body : ProgSem (σ ++ [v]) body r t s) : AppSem (Value.closure body σ) v r t s

inductive Complexity.RoseTreeMachine.WhileSem : Value → Data → Data → ℕ → ℕ → Prop

Iterates the closure bodyVal of a while_ loop, threading the accumulator. WhileSem bodyVal acc r t s means that, starting from accumulator acc, repeatedly applying bodyVal to the current accumulator eventually yields result r using t time and s space. Before each iteration the halting condition is checked on the current accumulator: iteration terminates (with the accumulator as result) when acc is empty or its head is empty. Otherwise bodyVal is applied and its result becomes the new accumulator. Non-terminating loops simply have no derivation.

• halt {bodyVal : Value} {acc : Data} (h_stop : acc.asList.head?.getD (Data.l []) = Data.l []) : WhileSem bodyVal acc acc acc.size acc.size
• step {bodyVal : Value} {acc v : Data} {t_b s_b : ℕ} {r : Data} {t_r s_r : ℕ} (h_cont : acc.asList.head?.getD (Data.l []) ≠ Data.l []) (h_app : AppSem bodyVal (Value.data acc) (Value.data v) t_b s_b) (h_rest : WhileSem bodyVal v r t_r s_r) : WhileSem bodyVal acc r (t_b + t_r) (max s_b s_r)

theorem Complexity.RoseTreeMachine.ProgSem.size_le {σ : List Value} {p : Prog} {v : Value} {t s : ℕ} (h : ProgSem σ p v t s) : v.size ≤ t ∧ v.size ≤ s

Producing a value costs at least its size, in both time and space. This holds because every ProgSem derivation either reads/builds the value directly (charging its size) or returns a value produced by a sub-derivation whose cost it includes. Provable by mutual induction over ProgSem/AppSem/WhileSem.

theorem Complexity.RoseTreeMachine.ProgSem.value_det {σ : List Value} {p : Prog} {v₁ : Value} {t₁ s₁ : ℕ} (h₁ : ProgSem σ p v₁ t₁ s₁) (v₂ : Value) (t₂ s₂ : ℕ) : ProgSem σ p v₂ t₂ s₂ → v₁ = v₂

Value-determinism of the relational semantics: a program evaluates to at most one value in a given environment. The mutually-defined AppSem/WhileSem relations are value-deterministic too. The potential branch overlaps (elim_nil/elim_cons, ifEq_then/ifEq_else) are ruled out by value-determinism of the scrutinee / compared values, supplied by the induction hypotheses.

def Complexity.RoseTreeMachine.Prog.ComputesInTimeAndSpace (p : Prog) (x y : Data) (t s : ℕ) : Prop

The program p computes the value y from the value x in time t and space s.

Equations

• p.ComputesInTimeAndSpace x y t s = Complexity.RoseTreeMachine.ProgSem [Complexity.RoseTreeMachine.Value.data x] p (Complexity.RoseTreeMachine.Value.data y) t s

def Complexity.RoseTreeMachine.Prog.ComputesBoolFunInTimeAndSpace (p : Prog) (f : List Bool → List Bool) (t s : ℕ → ℕ) : Prop

The program p computes the function f (on binary strings) in time t and space s. This is the main definition that defines complexity for this computation model.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.RoseTreeMachine.ComputableInOTime (f : List Bool → List Bool) (t : ℕ → ℕ) : Prop

The function f is computable in time t in the RTM model, up to constant factors

Equations

• Complexity.RoseTreeMachine.ComputableInOTime f t = ∃ (p : Complexity.RoseTreeMachine.Prog), ∃ (a : ℕ), ∃ (s : ℕ → ℕ), p.ComputesBoolFunInTimeAndSpace f (fun (n : ℕ) => a * t n + a) s

def Complexity.RoseTreeMachine.ComputableInOSpace (f : List Bool → List Bool) (s : ℕ → ℕ) : Prop

The function f is computable in space s in the RTM model, up to constant factors

Equations

• Complexity.RoseTreeMachine.ComputableInOSpace f s = ∃ (p : Complexity.RoseTreeMachine.Prog), ∃ (a : ℕ), ∃ (t : ℕ → ℕ), p.ComputesBoolFunInTimeAndSpace f t fun (n : ℕ) => a * s n + a

inductive Complexity.RoseTreeMachine.InPlace : Prog → Prop

The in-place (first-order) fragment of the functional language.

InPlace p holds when every fn in p occurs in an immediately-consumed position — as the operator of an app, or as the (curried) branch of an elim/while_. Consequently no closure ever escapes: every abstraction is created and used on the spot, so all values that flow through the environment are first-order Data. This is exactly the fragment a defunctionalising compiler targets, and it is closed under the operational semantics.

A Turing machine can directly implement this fragment without the need for closures: One tape is used for each "node" in the syntax tree.

• var {i : ℕ} : InPlace (Prog.var i)
• empty : InPlace Prog.empty
• cons {h t : Prog} (hh : InPlace h) (ht : InPlace t) : InPlace (h.cons t)
• elim {v emp body : Prog} (hv : InPlace v) (hemp : InPlace emp) (hbody : InPlace body) : InPlace (v.elim emp body.fn.fn)

  elim over an in-place value, empty branch, and a curried two-argument function branch fn (fn body) binding head and tail.

• ifEq {x y then_ else_ : Prog} (hx : InPlace x) (hy : InPlace y) (hthen : InPlace then_) (helse : InPlace else_) : InPlace (x.ifEq y then_ else_)
• while_ {init body : Prog} (hinit : InPlace init) (hbody : InPlace body) : InPlace (init.while_ body.fn)

  while_ whose body is a literal one-argument function fn body binding the accumulator.

• app {body arg : Prog} (hbody : InPlace body) (harg : InPlace arg) : InPlace (body.fn.app arg)

  app whose operator is a literal one-argument function fn body: this is a let, binding the value of arg and running body on the spot. The abstraction is consumed immediately, so no closure escapes. Nested applications of this form give multi-argument let-chains; arbitrary arities follow by repeated use of this constructor.