Library OracleLanguages.ProgrammingLanguage
Basic definitions about deterministic programming languages.
We specify a record signature whose inhabitants define a
deterministic programming language.
This signature requires a type state for the dynamically
changing part of the configuration while genv_type is the static
part of the configuration (typically containing the source code
and runtime constants and primitives).
This signature also requires that the semantics of the programming
language is described by a small-step reduction function step.
This reduction function is a partial function that may rewrite a
dynamic state into a new dynamic state.
For practical reasons, the dynamic state must be equipped with a
decidable equality.
Require Import Common.
Record language : Type :=
{
return_type : Type;
state : Type;
genv_type : Type;
step : genv_type → state → option state;
state_final : state → option return_type;
state_final_no_step : ∀ genv s v, state_final s = Some v → step genv s = None;
prog : Type;
initial_state : prog → genv_type × state;
genv_eq : genv_type → genv_type → Prop;
genv_eq_refl : ∀ genv, genv_eq genv genv;
genv_eq_sym : ∀ genv₁ genv₂, genv_eq genv₁ genv₂ → genv_eq genv₂ genv₁;
genv_eq_trans : ∀ genv₁ genv₂ genv₃,
genv_eq genv₁ genv₂ →
genv_eq genv₂ genv₃ →
genv_eq genv₁ genv₃;
genv_eq_dec : ∀ genv genv',
{genv_eq genv genv'} + {¬ genv_eq genv genv'};
state_eq : state → state → Prop;
state_eq_refl : ∀ S, state_eq S S;
state_eq_sym : ∀ S S', state_eq S S' → state_eq S' S;
state_eq_trans : ∀ S₁ S₂ S₃,
state_eq S₁ S₂ → state_eq S₂ S₃ → state_eq S₁ S₃;
state_eq_dec : ∀ S S',
{state_eq S S'} + {¬ state_eq S S'};
state_final_eq : ∀ S S',
state_eq S S' →
state_final S = state_final S';
step_eq : ∀ genv₁ genv₂ S₁ S₂ S₁' S₂',
genv_eq genv₁ genv₂ →
state_eq S₁ S₂ →
step genv₁ S₁ = Some S₁' →
step genv₂ S₂ = Some S₂' →
state_eq S₁' S₂';
step_eq' : ∀ genv₁ genv₂ S₁ S₂,
genv_eq genv₁ genv₂ →
state_eq S₁ S₂ →
step genv₁ S₁ = None ↔ step genv₂ S₂ = None
}.
We call a configuration the pair of the static global
environment and the dynamic state of a program.
Definition configuration (L : language) : Type := genv_type L × state L.
Definition initial_configuration {L : language} (p : prog L) :=
initial_state L p.
Definition configuration_eq {L : language} (c₁ c₂ : configuration L) :=
genv_eq L (fst c₁) (fst c₂) ∧ state_eq L (snd c₁) (snd c₂).
Definition opt_state_eq {L : language} (oS₁ oS₂ : option (state L)) : Prop :=
(oS₁ = None ∧ oS₂ = None)
∨ ∃ S₁ S₂, oS₁ = Some S₁ ∧ oS₂ = Some S₂ ∧ state_eq L S₁ S₂.
Lemma opt_state_eq_dec:
∀ {L : language} (oS₁ oS₂ : option (state L)),
{ opt_state_eq oS₁ oS₂ } + { ¬ opt_state_eq oS₁ oS₂ }.
Lemma state_eq__opt_state_eq:
∀ {L} (S₁ S₂ : state L),
state_eq L S₁ S₂ ↔ opt_state_eq (Some S₁) (Some S₂).
Lemma opt_state_eq_Some_r__state_eq:
∀ {L} (S : state L) (oS : option (state L)),
opt_state_eq oS (Some S) →
∃ S', oS = Some S' ∧ state_eq L S' S.
Lemma opt_state_eq_refl:
∀ {L} (oS : option (state L)),
opt_state_eq oS oS.
Lemma opt_state_eq_sym:
∀ {L} (oS₁ oS₂ : option (state L)),
opt_state_eq oS₁ oS₂ → opt_state_eq oS₂ oS₁.
Lemma opt_state_eq_trans:
∀ {L} (oS₁ oS₂ oS₃ : option (state L)),
opt_state_eq oS₁ oS₂ → opt_state_eq oS₂ oS₃ → opt_state_eq oS₁ oS₃.
We use nsteps to repeatedly call the reduction function step.
As step is a partial function, so is nsteps.
We also define a total function nsteps' that always return a
state together with the number of reduction steps it could not
perform.
Hence, if nsteps' n state = (state', 0), the reduction
function has been applied n times successfully (nsteps_nsteps'_0_iff).
On the other hand, if nsteps' n state = (state', S n'), state' is
guaranteed to be a stuck state and was obtained by rewriting state n - S n'
times.
Definition nsteps {lang : language} (genv : genv_type lang)
(n : nat) (S : state lang) : option (state lang) :=
napply (step lang genv) n S.
Definition nsteps' {lang : language} (genv : genv_type lang)
(n : nat) (S : state lang) : state lang × nat :=
napply' (step lang genv) n S.
Lemma nsteps_eq:
∀ {L : language} (genv₁ genv₂ : genv_type L) (S₁ S₂ : state L) (n : nat),
genv_eq L genv₁ genv₂ →
state_eq L S₁ S₂ →
opt_state_eq (nsteps genv₁ n S₁) (nsteps genv₂ n S₂).
Lemma nsteps_plus_0:
∀ {L : language} (genv : genv_type L) {n₁ n₂ : nat} (S₁ : state L),
nsteps genv (n₁ + n₂) S₁ = nsteps genv n₁ S₁ >>= λ S₂, nsteps genv n₂ S₂.
Lemma nsteps_plus_1:
∀ {L : language} (genv : genv_type L) {n₁ n₂ : nat} (S₁ S₂ : state L),
nsteps genv n₁ S₁ = Some S₂ → nsteps genv (n₁ + n₂) S₁ = nsteps genv n₂ S₂.
Lemma nsteps_plus_1':
∀ {L : language} (genv : genv_type L) {n₁ n₂ : nat} (S₁ S₂ : state L),
opt_state_eq (nsteps genv n₁ S₁) (Some S₂) →
opt_state_eq (nsteps genv (n₁ + n₂) S₁) (nsteps genv n₂ S₂).
Lemma nsteps_plus_2:
∀ {L} {genv : genv_type L} n n' S S',
nsteps genv (n + n') S = Some S' →
∃ S₁,
nsteps genv n S = Some S₁.
Definition terminates {L} genv S :=
∃ n S', nsteps genv n S = Some S' ∧ step L genv S' = None.
Require Import Omega.
Lemma nsteps_split_helper:
∀ {L} genv n n' S S' oS',
nsteps genv n S = Some S' →
step L genv S' = None →
opt_state_eq (nsteps genv n' S) oS' →
(n' = n)
∨ (∃ S', n > n' ∧ nsteps genv n' S = Some S')
∨ (n' > n ∧ nsteps genv n' S = None).