Library OracleLanguages.ReductionTrace
Basic definitions about reduction traces.
We introduce reduction traces for any deterministic programming
language coinductively. Reachability and convergence are defined
on top of this notion.
While we will often abusively refer to potentially infinite non-empty
lists of configurations as traces, actual reduction traces are
characterized by the following trace predicate:
CoInductive trace (L : language) :
configuration L → coplist (configuration L) → Prop :=
| TFinal : ∀ genv state,
step L genv state = None →
trace L (genv, state) (CSingle _ (genv, state))
| TStep : ∀ genv state S' tr,
step L genv state = Some S' →
trace L (genv, S') tr →
trace L (genv, state) (CCons _ (genv, state) tr).
We also provide a variant trace' of the trace predicate that
hides the precise configuration the trace starts from:
Definition trace' (L : language) (l : coplist (configuration L)) : Prop :=
trace L (first l) l.
Lemma trace_first {L : language}:
∀ (c : configuration L) l, trace L c l → first l = c.
Lemma trace_trace':
∀ L l, trace' L l ↔ (∃ c, trace L c l).
Converging and crashing traces are characterized by inductive predicates:
Inductive nsteps_converging_trace {L : language}
: nat → coplist (configuration L) → Prop :=
| FinallyConverges:
∀ c result,
state_final L (snd c) = Some result →
nsteps_converging_trace 0 (CSingle _ c)
| CConsConverges : ∀ c tr n,
nsteps_converging_trace n tr →
nsteps_converging_trace (S n) (CCons _ c tr).
Inductive nsteps_crashing_trace {L : language}
: nat → coplist (configuration L) → Prop :=
| FinallyCrashes:
∀ c,
step L (fst c) (snd c) = None →
state_final L (snd c) = None →
nsteps_crashing_trace 0 (CSingle _ c)
| CConsCrashes : ∀ c tr n,
nsteps_crashing_trace n tr →
nsteps_crashing_trace (S n) (CCons _ c tr).
CoFixpoint traceFrom {L : language} (c : configuration L) : coplist (configuration L) :=
match step L (fst c) (snd c) with
| None ⇒
CSingle _ c
| Some state' ⇒
CCons _ c (traceFrom (fst c, state'))
end.
Lemma traceFrom_trace:
∀ L (c : configuration L),
trace L c (traceFrom c).
Definition program_trace (L : language) (p : prog L) :=
traceFrom (initial_configuration p).
Lemma nsteps_skipn:
∀ L tr n genv S S',
trace L (genv, S) tr →
opt_state_eq (nsteps genv n S) (Some S') →
∃ tr' S'',
skipn n tr = Some tr'
∧ trace L (genv, S'') tr'
∧ state_eq L S'' S'.
CoInductive included_subtrace {L : language}
: coplist (configuration L) → coplist (configuration L) → Prop :=
| SameFirst:
∀ tr₁ tr₂,
configuration_eq (first tr₁) (first tr₂) →
(∀ tr₁',
next tr₁ = Some tr₁' →
∃ tr₂', next tr₂ = Some tr₂' ∧ included_subtrace tr₁' tr₂') →
included_subtrace tr₁ tr₂
| Stutter:
∀ tr₁ tr₁' tr₂,
configuration_eq (first tr₁) (first tr₂) →
next tr₁ = Some tr₁' →
included_subtrace tr₁' tr₂ →
included_subtrace tr₁ tr₂
| IgnoreFirstSN:
∀ n tr₁ tr₂ tr₂',
skipn (S n) tr₂ = Some tr₂' →
included_subtrace tr₁ tr₂' →
included_subtrace tr₁ tr₂.