LOOP language

This file defines LOOP, a simple imperative nonreversible programming language that precisely captures all the primitive recursive functions.

Notations

• [x ↦ v] stands for update emp x v where emp is the empty Store (set the value of x to v in emp).
• σ[x ↦ v] stands for update σ x v (set the value of x to v in σ).

Consecutive updates can be concatenated as σ[x ↦ v₁][x ↦ v₂].

Implementation notes

A LOOP State is defined as an Option Store to provide a uniform structure for both LOOP and SCORE states, simplifying the management of the notion of equivalence. The term none can be interpreted as the failure state, even though this is not defined in the language specifications, nor is meaningful.

References

See [MR67] for the original account on LOOP language.

def LOOP.Store : Type

A Store provides an abstract representation of memory in the form of a total function from Ident to Nat.

Equations

• LOOP.Store = (Ident → ℕ)

def LOOP.Store.emp : LOOP.Store

An empty Store maps every identifier to zero.

Equations

• LOOP.Store.emp x = 0

def LOOP.Store.update (σ : LOOP.Store) (x : Ident) (v : ℕ) : LOOP.Store

Updates a Store by mapping the register identified by x to a new value v.

Equations

• (σ[x ↦ v]) y = if x = y then v else σ y

def LOOP.Store.«term[_↦_]» : Lean.ParserDescr

Equations

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

def LOOP.Store.«term_[_↦_]» : Lean.TrailingParserDescr

Equations

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

@[simp]

theorem LOOP.Store.update_same {σ : LOOP.Store} {x : Ident} {y : Ident} {v : ℕ} : x = y → (σ[x ↦ v]) y = v

If x = y then the current value of y in σ[x ↦ v] is v.

@[simp]

theorem LOOP.Store.update_other {σ : LOOP.Store} {x : Ident} {y : Ident} {v : ℕ} : x ≠ y → (σ[x ↦ v]) y = σ y

If x ≠ y then the current value of y in σ[x ↦ v] is σ y.

@[simp]

theorem LOOP.Store.update_no_update {σ : LOOP.Store} {x : Ident} : σ[x ↦ σ x] = σ

Updating a variable to its current value produces no change.

@[reducible, inline]

abbrev LOOP.State : Type

A State can be a Store or a failure.

Equations

• LOOP.State = Option LOOP.Store

def LOOP.State.«term⊥» : Lean.ParserDescr

Equations

• LOOP.State.«term⊥» = Lean.ParserDescr.node `LOOP.State.term⊥ 1024 (Lean.ParserDescr.symbol "⊥")

inductive LOOP.Com : Type

A LOOP program is a sequence of commands chosen from skip, clearing a register, incrementing a register, copying one register to another, composing two commands, and iterating over a finite number of steps.

• SKIP: LOOP.Com
• ZER: Ident → LOOP.Com
• ASN: Ident → Ident → LOOP.Com
• INC: Ident → LOOP.Com
• SEQ: LOOP.Com → LOOP.Com → LOOP.Com
• LOOP: Ident → LOOP.Com → LOOP.Com

instance LOOP.instBEqCom : BEq LOOP.Com

Equations

• LOOP.instBEqCom = { beq := LOOP.beqCom✝ }

def LOOP.Com.«term_;;_» : Lean.TrailingParserDescr

Equations

• LOOP.Com.«term_;;_» = Lean.ParserDescr.trailingNode `LOOP.Com.term_;;_ 80 81 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol ";;") (Lean.ParserDescr.cat `term 80))

def LOOP.Com.ids (P : LOOP.Com) : Finset Ident

Computes the set of identifiers that appear in a LOOP command.

Equations

• LOOP.Com.SKIP.ids = ∅
• (LOOP.Com.ZER x).ids = {x}
• (LOOP.Com.ASN x y).ids = {x, y}
• (LOOP.Com.INC x).ids = {x}
• (P_2;;Q).ids = P_2.ids ∪ Q.ids
• (LOOP.Com.LOOP x P_2).ids = {x} ∪ P_2.ids

def LOOP.Com.comToString (indLv : ℕ) (P : LOOP.Com) : String

Computes the string representation of a LOOP command.

Equations

• One or more equations did not get rendered due to their size.
• LOOP.Com.comToString indLv LOOP.Com.SKIP = toString "" ++ toString (LOOP.Com.comToString.ind indLv) ++ toString "SKIP"
• LOOP.Com.comToString indLv (LOOP.Com.ZER x) = toString "" ++ toString (LOOP.Com.comToString.ind indLv) ++ toString "" ++ toString x ++ toString " = 0"
• LOOP.Com.comToString indLv (LOOP.Com.ASN x y) = toString "" ++ toString (LOOP.Com.comToString.ind indLv) ++ toString "" ++ toString x ++ toString " = " ++ toString y ++ toString ""
• LOOP.Com.comToString indLv (LOOP.Com.INC x) = toString "" ++ toString (LOOP.Com.comToString.ind indLv) ++ toString "" ++ toString x ++ toString " += 1"
• LOOP.Com.comToString indLv (P_2;;Q) = toString "" ++ toString (LOOP.Com.comToString indLv P_2) ++ toString ";\n" ++ toString (LOOP.Com.comToString indLv Q) ++ toString ""

def LOOP.Com.comToString.ind (indLv : ℕ) : String

Equations

• LOOP.Com.comToString.ind Nat.zero = ""
• LOOP.Com.comToString.ind m.succ = " " ++ LOOP.Com.comToString.ind m

instance LOOP.Com.instToString : ToString LOOP.Com

Equations

• LOOP.Com.instToString = { toString := LOOP.Com.comToString 0 }

def LOOP.eval (P : LOOP.Com) (s : LOOP.State) : LOOP.State

Interpreter for LOOP. The interpreter takes as input a Com and an evaluation State and outputs the resulting State obtained by applying the command to the initial state.

Equations

• LOOP.eval P none = none
• LOOP.eval LOOP.Com.SKIP (some σ) = some σ
• LOOP.eval (LOOP.Com.ZER x) (some σ) = some (σ[x ↦ 0])
• LOOP.eval (LOOP.Com.ASN x y) (some σ) = some (σ[x ↦ σ y])
• LOOP.eval (LOOP.Com.INC x) (some σ) = some (σ[x ↦ σ x + 1])
• LOOP.eval (P_2;;Q) (some σ) = LOOP.eval Q (LOOP.eval P_2 (some σ))
• LOOP.eval (LOOP.Com.LOOP x P_2) (some σ) = (fun (σ' : LOOP.State) => LOOP.eval P_2 σ')^[σ x] (some σ)