Mechanization of operational semantics.
Require Import String.
Require Import List.
Require Import Sequences.
Open Scope string_scope.
Open Scope list_scope.
Abstract syntax of the language
Definition var:
Type :=
string.
Definition var_eq:
forall (
v1 v2:
var), {
v1=
v2} + {
v1<>
v2} :=
string_dec.
Definition const:
Type :=
nat.
Inductive term:
Type :=
|
Var:
var ->
term (* variable *)
|
Const:
const ->
term (* constant *)
|
Fun:
var ->
term ->
term (* function abstraction *)
|
App:
term ->
term ->
term.
(* function application *)
subst x b a replaces x by b in a.
Warning: not capture-avoiding! b must be closed.
Fixpoint subst (
x:
var) (
b:
term) (
a:
term) {
struct a}:
term :=
match a with
|
Var y =>
if var_eq x y then b else Var y
|
Const n =>
Const n
|
Fun y a1 =>
Fun y (
if var_eq x y then a1 else subst x b a1)
|
App a1 a2 =>
App (
subst x b a1) (
subst x b a2)
end.
Values are either constants or functions.
Inductive isvalue:
term ->
Prop :=
|
isvalue_const:
forall c,
isvalue (
Const c)
|
isvalue_fun:
forall x a,
isvalue (
Fun x a).
Hint Constructors isvalue:
sem.
Operational semantics
Reduction semantics (small-step)
One step of reduction, in SOS style.
Inductive red:
term ->
term ->
Prop :=
|
red_beta:
forall x a v,
(* beta-v reduction at top of term *)
isvalue v ->
red (
App (
Fun x a)
v) (
subst x v a)
|
red_app_l:
forall a1 a2 b,
(* reduction to the left of an application *)
red a1 a2 ->
red (
App a1 b) (
App a2 b)
|
red_app_r:
forall v b1 b2,
(* reduction to the right of an application *)
isvalue v ->
red b1 b2 ->
red (
App v b1) (
App v b2).
Hint Constructors red:
sem.
Values do not reduce.
Lemma value_irred:
forall a,
isvalue a ->
irred red a.
Proof.
destruct 1;
unfold irred;
intros;
red;
intros;
inversion H.
Qed.
Determinism of one-step reduction.
Lemma red_deterministic:
forall a b c,
red a b ->
red a c ->
b =
c.
Proof.
intros a b c R.
revert a b R c.
induction 1;
intros c R';
inversion R';
subst.
auto.
inversion H3.
elim (
value_irred v H b2 H4).
inversion R.
f_equal;
auto.
elim (
value_irred a1 H1 a2 R).
elim (
value_irred b1 H3 b2 R).
elim (
value_irred v H a2 H3).
f_equal;
auto.
Qed.
The three possible outcomes of an execution.
Definition terminates (
a:
term) (
v:
term) :
Prop :=
star red a v /\
isvalue v.
Definition diverges (
a:
term) :
Prop :=
infseq red a.
Definition goes_wrong (
a:
term) :
Prop :=
exists b,
star red a b /\
irred red b /\ ~
isvalue b.
Natural semantics (big-step)
For termination.
Inductive eval:
term ->
term ->
Prop :=
|
eval_const:
forall c,
eval (
Const c) (
Const c)
|
eval_fun:
forall x a,
eval (
Fun x a) (
Fun x a)
|
eval_app:
forall a b x c vb v,
eval a (
Fun x c) ->
eval b vb ->
eval (
subst x vb c)
v ->
eval (
App a b)
v.
Lemma eval_isvalue:
forall a b,
eval a b ->
isvalue b.
Proof.
induction 1; auto with sem.
Qed.
For divergence.
CoInductive evalinf:
term ->
Prop :=
|
evalinf_app_l:
forall a b,
evalinf a ->
evalinf (
App a b)
|
evalinf_app_r:
forall a b va,
eval a va ->
evalinf b ->
evalinf (
App a b)
|
evalinf_app_f:
forall a b x c vb,
eval a (
Fun x c) ->
eval b vb ->
evalinf (
subst x vb c) ->
evalinf (
App a b).
An example of a term that diverges.
Definition delta :=
Fun "
x" (
App (
Var "
x") (
Var "
x")).
Definition omega :=
App delta delta.
Lemma evalinf_omega:
evalinf omega.
Proof.
Hint Constructors eval evalinf:
sem.
Hint Resolve eval_isvalue:
sem.
Equivalence small-step / big-step
Context lemmas for reduction sequences.
Lemma star_red_app_l:
forall a1 a2 b,
star red a1 a2 ->
star red (
App a1 b) (
App a2 b).
Proof.
induction 1; intros; eauto with sem sequences.
Qed.
Lemma star_red_app_r:
forall v a1 a2,
isvalue v ->
star red a1 a2 ->
star red (
App v a1) (
App v a2).
Proof.
induction 2; intros; eauto with sem sequences.
Qed.
If a evaluates to v, there exists a finite reduction sequence from a to v.
Lemma eval_star_red:
forall a v,
eval a v ->
star red a v.
Proof.
If a reduces to v in zero, one or several steps, then a evaluates to v.
Lemma eval_value:
forall v,
isvalue v ->
eval v v.
Proof.
induction 1; intros; constructor.
Qed.
Hint Resolve eval_value:
sem.
Lemma red_eval:
forall a b,
red a b ->
forall v,
eval b v ->
eval a v.
Proof.
induction 1; intros.
- eauto with sem.
- inversion H0. eauto with sem.
- inversion H1. eauto with sem.
Qed.
Lemma star_red_eval:
forall a v,
star red a v ->
isvalue v ->
eval a v.
Proof.
Hint Resolve star_red_eval:
sem.
Corollary: equivalence between eval and small-step termination.
Theorem eval_terminates:
forall a v,
terminates a v <->
eval a v.
Proof.
If a diverges according to evalinf, it can make one step of reduction
to a term that still diverges according to evalinf.
Lemma evalinf_red:
forall a,
evalinf a ->
exists b,
red a b /\
evalinf b.
Proof.
induction a;
intros;
inversion H;
subst.
- (* function part evaluates infinitely *)
destruct (
IHa1 H1)
as [
a1' [
R E]].
exists (
App a1'
a2);
eauto with sem.
- (* function part evaluates finitely,
argument evaluates infinitely *)
destruct (
IHa2 H3)
as [
a2' [
R E]].
assert (
S:
star red a1 va)
by (
apply eval_star_red;
auto).
inversion S;
subst.
+ (* function part was already a value *)
exists (
App va a2');
eauto with sem.
+ (* function part evaluates *)
exists (
App b a2);
eauto 6
with sem.
- (* function and argument parts evaluate finitely,
beta-redex evaluates infinitely *)
assert (
S1:
star red a1 (
Fun x c))
by (
apply eval_star_red;
auto).
assert (
S2:
star red a2 vb)
by (
apply eval_star_red;
auto).
inversion S1;
subst; [
inversion S2;
subst|
idtac].
+ (* function part and argument part were already values *)
exists (
subst x vb c);
eauto with sem.
+ (* function part was already a value, argument part reduces *)
exists (
App (
Fun x c)
b);
eauto 6
with sem.
+ (* function part reduces *)
exists (
App b a2);
eauto with sem.
Qed.
As a consequence, if a diverges according to evalinf, there exists
an infinite sequence of reductions starting with a.
Lemma evalinf_infseq_red:
forall a,
evalinf a ->
infseq red a.
Proof.
cofix COINDHYP.
intros.
destruct (
evalinf_red _ H)
as [
b [
R E]].
apply infseq_step with b.
auto.
apply COINDHYP.
auto.
Qed.
Conversely, if there exists an infinite sequence of reductions starting with a,
then a diverges according to evalinf.
Lemma infseq_red_evalinf:
forall a,
infseq red a ->
evalinf a.
Proof.
cofix COINDHYP.
intros.
destruct a;
try (
inversion H;
inversion H0;
fail).
elim (
infseq_or_finseq red a1).
- (* a1 evaluates infinitely *)
intro REDINF1.
apply evalinf_app_l.
apply COINDHYP.
assumption.
- (* a1 evaluates finitely *)
intros [
n1 [
REDM1 NOTRED1]].
assert (
REDINF1:
infseq red (
App n1 a2)).
eapply infseq_star_inv;
eauto.
exact red_deterministic.
apply star_red_app_l;
auto.
assert (
ISVAL1:
isvalue n1).
inversion REDINF1.
inversion H0.
constructor.
elim (
NOTRED1 _ H6).
assumption.
elim (
infseq_or_finseq red a2).
+ (* a2 evaluates infinitely *)
intro REDINF2.
apply evalinf_app_r with n1.
apply star_red_eval;
assumption.
apply COINDHYP.
assumption.
+ (* a2 evaluates finitely as well *)
intros [
n2 [
REDM2 NOTRED2]].
assert (
REDINF2:
infseq red (
App n1 n2)).
eapply infseq_star_inv;
eauto.
exact red_deterministic.
apply star_red_app_r;
auto.
assert (
NEXTRED:
exists x,
exists c,
n1 =
Fun x c /\
isvalue n2 /\
infseq red (
subst x n2 c)).
inversion REDINF2.
inversion H0.
subst b.
exists x;
exists a0.
tauto.
elim (
NOTRED1 _ H6).
elim (
NOTRED2 _ H7).
destruct NEXTRED as [
x [
c [
A [
B C]]]].
subst n1.
apply evalinf_app_f with x c n2.
apply star_red_eval;
assumption.
apply star_red_eval;
assumption.
apply COINDHYP.
assumption.
Qed.
Corollary: equivalence between evalinf and small-step divergence.
Theorem evalinf_diverges:
forall a,
diverges a <->
evalinf a.
Proof.