SCORE language

This file defines SCORE, a minimal reversible programming language designed as a reversible adaptation of LOOP. SCORE can be understood as an extension of SRL [Mat03] that operates on variables represented by stacks of integers.

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₂].

• P⁻¹ stands for inv P (the inverse program of P).

def SCORE.Store : Type

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

Equations

• SCORE.Store = (Ident → List ℤ)

def SCORE.Store.emp : SCORE.Store

An empty Store maps every identifier to the empty list.

Equations

• SCORE.Store.emp x = []

def SCORE.Store.update (σ : SCORE.Store) (x : Ident) (l : List ℤ) : SCORE.Store

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

Equations

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

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

Equations

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

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

Equations

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

@[simp]

theorem SCORE.Store.update_same {σ : SCORE.Store} {x : Ident} {y : Ident} {l : List ℤ} : x = y → (σ[x ↦ l]) y = l

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

@[simp]

theorem SCORE.Store.update_other {σ : SCORE.Store} {x : Ident} {y : Ident} {l : List ℤ} : x ≠ y → (σ[x ↦ l]) y = σ y

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

@[simp]

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

Updating a variable to its current value produces no change.

@[simp]

theorem SCORE.Store.update_shrink {σ : SCORE.Store} {x : Ident} {l₁ : List ℤ} {l₂ : List ℤ} : σ[x ↦ l₁][x ↦ l₂] = σ[x ↦ l₂]

Two consecutive updates to the same variable can be compressed into a single update.

theorem SCORE.Store.update_no_update_cons {σ : SCORE.Store} {x : Ident} {v : ℤ} : (σ x).head? = some v → σ[x ↦ v :: (σ x).tail] = σ

Alternative version of update_no_update that considers the structure of the list.

theorem SCORE.Store.update_swap {σ : SCORE.Store} {x : Ident} {y : Ident} {l₁ : List ℤ} {l₂ : List ℤ} : x ≠ y → σ[x ↦ l₁][y ↦ l₂] = σ[y ↦ l₂][x ↦ l₁]

The order in which two different variables are updated is not significant.

@[reducible, inline]

abbrev SCORE.State : Type

A State can be a Store or a failure.

Equations

• SCORE.State = Option SCORE.Store

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

Equations

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

inductive SCORE.Com : Type

A SCORE program is a sequence of commands chosen from skip, extending a stack, decreasing a stack, incrementing the top of a stack, decrementing the top of a stack, composing two commands, and iterating over a finite number of steps.

• SKIP: SCORE.Com
• CON: Ident → SCORE.Com
• NOC: Ident → SCORE.Com
• DEC: Ident → SCORE.Com
• INC: Ident → SCORE.Com
• SEQ: SCORE.Com → SCORE.Com → SCORE.Com
• FOR: Ident → SCORE.Com → SCORE.Com

instance SCORE.instBEqCom : BEq SCORE.Com

Equations

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

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

Equations

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

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

Computes the string representation of a LOOP command.

Equations

• One or more equations did not get rendered due to their size.
• SCORE.Com.comToString indLv SCORE.Com.SKIP = toString "" ++ toString (SCORE.Com.comToString.ind indLv) ++ toString "SKIP"
• SCORE.Com.comToString indLv (SCORE.Com.CON x) = toString "" ++ toString (SCORE.Com.comToString.ind indLv) ++ toString "CON " ++ toString x ++ toString ""
• SCORE.Com.comToString indLv (SCORE.Com.NOC x) = toString "" ++ toString (SCORE.Com.comToString.ind indLv) ++ toString "NOC " ++ toString x ++ toString ""
• SCORE.Com.comToString indLv (SCORE.Com.DEC x) = toString "" ++ toString (SCORE.Com.comToString.ind indLv) ++ toString "DEC " ++ toString x ++ toString ""
• SCORE.Com.comToString indLv (SCORE.Com.INC x) = toString "" ++ toString (SCORE.Com.comToString.ind indLv) ++ toString "INC " ++ toString x ++ toString ""
• SCORE.Com.comToString indLv (P_2;;Q) = toString "" ++ toString (SCORE.Com.comToString indLv P_2) ++ toString ";\n" ++ toString (SCORE.Com.comToString indLv Q) ++ toString ""

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

Equations

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

instance SCORE.Com.instToString : ToString SCORE.Com

Equations

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

def SCORE.inv (P : SCORE.Com) : SCORE.Com

Equations

• SCORE.Com.SKIP⁻¹ = SCORE.Com.SKIP
• (SCORE.Com.CON x)⁻¹ = SCORE.Com.NOC x
• (SCORE.Com.NOC x)⁻¹ = SCORE.Com.CON x
• (SCORE.Com.DEC x)⁻¹ = SCORE.Com.INC x
• (SCORE.Com.INC x)⁻¹ = SCORE.Com.DEC x
• (P_2;;Q)⁻¹ = Q⁻¹;;P_2⁻¹
• (SCORE.Com.FOR x P_2)⁻¹ = SCORE.Com.FOR x P_2⁻¹

def SCORE.«term_⁻¹» : Lean.TrailingParserDescr

Equations

• SCORE.«term_⁻¹» = Lean.ParserDescr.trailingNode `SCORE.term_⁻¹ 1024 1024 (Lean.ParserDescr.symbol "⁻¹")

theorem SCORE.inv_inv (P : SCORE.Com) : P⁻¹⁻¹ = P

The inverse of the inverse program of P is P itself.

Interpreter

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

Interpreter for SCORE. 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

• One or more equations did not get rendered due to their size.
• SCORE.eval P none = none
• SCORE.eval SCORE.Com.SKIP (some σ) = some σ
• SCORE.eval (SCORE.Com.CON x) (some σ) = some (σ[x ↦ 0 :: σ x])
• SCORE.eval (SCORE.Com.NOC x) (some σ) = match (σ x).head? with | some 0 => some (σ[x ↦ (σ x).tail]) | x => none
• SCORE.eval (SCORE.Com.DEC x) (some σ) = match (σ x).head? with | some v => some (σ[x ↦ (v - 1) :: (σ x).tail]) | none => none
• SCORE.eval (SCORE.Com.INC x) (some σ) = match (σ x).head? with | some v => some (σ[x ↦ (v + 1) :: (σ x).tail]) | none => none
• SCORE.eval (P_2;;Q) (some σ) = SCORE.eval Q (SCORE.eval P_2 (some σ))

def SCORE.evalI (P : SCORE.Com) (s : SCORE.State) : SCORE.State

Reverse interpreter for SCORE. The interpreter takes as input a Com and an evaluation State and outputs the resulting State obtained by applying the inverse of the command to the initial state.

Invertibility

theorem SCORE.invertible_SKIP {s : SCORE.State} {t : SCORE.State} : SCORE.eval SCORE.Com.SKIP s = t ∧ t ≠ none ↔ SCORE.eval SCORE.Com.SKIP⁻¹ t = s ∧ s ≠ none

theorem SCORE.invertible_CON {s : SCORE.State} {t : SCORE.State} {x : Ident} : SCORE.eval (SCORE.Com.CON x) s = t ∧ t ≠ none ↔ SCORE.eval (SCORE.Com.CON x)⁻¹ t = s ∧ s ≠ none

theorem SCORE.invertible_NOC {s : SCORE.State} {t : SCORE.State} {x : Ident} : SCORE.eval (SCORE.Com.NOC x) s = t ∧ t ≠ none ↔ SCORE.eval (SCORE.Com.NOC x)⁻¹ t = s ∧ s ≠ none

theorem SCORE.invertible_DEC {s : SCORE.State} {t : SCORE.State} {x : Ident} : SCORE.eval (SCORE.Com.DEC x) s = t ∧ t ≠ none ↔ SCORE.eval (SCORE.Com.DEC x)⁻¹ t = s ∧ s ≠ none

theorem SCORE.invertible_INC {s : SCORE.State} {t : SCORE.State} {x : Ident} : SCORE.eval (SCORE.Com.INC x) s = t ∧ t ≠ none ↔ SCORE.eval (SCORE.Com.INC x)⁻¹ t = s ∧ s ≠ none

theorem SCORE.invertible_SEQ {s : SCORE.State} {t : SCORE.State} {P : SCORE.Com} {Q : SCORE.Com} (ih₁ : ∀ {s t : SCORE.State}, SCORE.eval P s = t ∧ t ≠ none ↔ SCORE.eval P⁻¹ t = s ∧ s ≠ none) (ih₂ : ∀ {s t : SCORE.State}, SCORE.eval Q s = t ∧ t ≠ none ↔ SCORE.eval Q⁻¹ t = s ∧ s ≠ none) : SCORE.eval (P;;Q) s = t ∧ t ≠ none ↔ SCORE.eval (P;;Q)⁻¹ t = s ∧ s ≠ none

theorem SCORE.invertible {s : SCORE.State} {t : SCORE.State} {P : SCORE.Com} : SCORE.eval P s = t ∧ t ≠ none ↔ SCORE.eval P⁻¹ t = s ∧ s ≠ none