Commit 2203b568 authored by Andrew Hirsch's avatar Andrew Hirsch
Browse files

Comments for local languages.

parent 867f7f59
(* (*
Module type for the local language. Module type for the local language.
We can instantiate this module type with any We can instantiate this module type with any number of languages, as we can see in the
number of languages, as we can see in the examples. examples.
*) *)
Module Type LocalLang. Module Type LocalLang.
(* (*
The local language is an expression-based language. The local language is an expression-based language. We assume that expressions have
We assume that expressions have decidable syntactic equality. decidable syntactic equality. This is a pretty weak assumption for syntax.
This is a pretty weak assumption for syntax.
*) *)
Parameter Expr : Set. Parameter Expr : Set.
Parameter ExprEqDec : forall e1 e2 : Expr, {e1 = e2} + {e1 <> e2}. Parameter ExprEqDec : forall e1 e2 : Expr, {e1 = e2} + {e1 <> e2}.
(* Since we use de Bruijn indices, we represent variables as (*
natural numbers. We don't require any sort of binders in Since we use de Bruijn indices, we represent variables as natural numbers. We don't
the local language, so these don't necessarily count to require any sort of binders in the local language, so these don't necessarily count
the relevant binder. However, in our examples they do. *) to the relevant binder. However, in our examples they do.
*)
Parameter ExprVar : nat -> Expr. Parameter ExprVar : nat -> Expr.
(* An expression is closed above `n` if variables above `n` (*
do not appear free in the expression. Clearly, if An expression is closed above `n` if variables above `n` do not appear free in the
an expression is closed above `0`, then it contains expression. Clearly, if an expression is closed above `0`, then it contains no free
no free variables. variables.
The property of being closed above is monotonic. The property of being closed above is monotonic. Moreover, variables are always closed
Moreover, variables are always closed above above anything greater than themselves.
anything greater than themselves.
*) *)
Parameter ExprClosedAbove : nat -> Expr -> Prop. Parameter ExprClosedAbove : nat -> Expr -> Prop.
Definition ExprClosed := ExprClosedAbove 0. Definition ExprClosed := ExprClosedAbove 0.
...@@ -36,22 +35,19 @@ Module Type LocalLang. ...@@ -36,22 +35,19 @@ Module Type LocalLang.
Parameter ExprVarClosed : forall n m, ExprClosedAbove n (ExprVar m) <-> m < n. Parameter ExprVarClosed : forall n m, ExprClosedAbove n (ExprVar m) <-> m < n.
(* (*
Values are a subset of expressions (here represented Values are a subset of expressions (here represented as a property of expressions.
as a property of expressions. These are always closed. These are always closed. This restriction is necessary for communication to typecheck
This restriction is necessary for communication to in Pirouette.
typecheck in Pirouette.
*) *)
Parameter ExprVal : Expr -> Prop. Parameter ExprVal : Expr -> Prop.
Parameter ExprValuesClosed : forall v : Expr, ExprVal v -> ExprClosed v. Parameter ExprValuesClosed : forall v : Expr, ExprVal v -> ExprClosed v.
(* (*
Local languages need to define a(n infinite) Local languages need to define a(n infinite) substitution operator. This replaces all
substitution operator. This replaces all variables variables in the expression with new subexpressions. We also consider a renaming
in the expression with new subexpressions. We also operation, which allows us to substitute variables more easily with other variables.
consider a renaming operation, which allows us to This can be defined via the "specification" equation below, but it is often better to
substitute variables more easily with other variables. define it seperately.
This can be defined via the "specification" equation
below, but it is often better to define it seperately.
*) *)
Parameter ExprSubst : Expr -> (nat -> Expr) -> Expr. Parameter ExprSubst : Expr -> (nat -> Expr) -> Expr.
Parameter ExprRename : Expr -> (nat -> nat) -> Expr. Parameter ExprRename : Expr -> (nat -> nat) -> Expr.
...@@ -60,8 +56,9 @@ Module Type LocalLang. ...@@ -60,8 +56,9 @@ Module Type LocalLang.
Parameter ExprRenameSpec : forall (e : Expr) (ξ : nat -> nat), Parameter ExprRenameSpec : forall (e : Expr) (ξ : nat -> nat),
e e| ξ⟩ = e [e| fun n => ExprVar (ξ n)]. e e| ξ⟩ = e [e| fun n => ExprVar (ξ n)].
(* Substitution must correctly replace a variable. (*
This allows us to show that renaming must do the same thing. Substitution must correctly replace a variable. This allows us to show that renaming
must do the same thing.
*) *)
Parameter ExprSubstVar : forall n σ, (ExprVar n ) [e| σ] = σ n. Parameter ExprSubstVar : forall n σ, (ExprVar n ) [e| σ] = σ n.
Lemma ExprRenameVar : forall n ξ, (ExprVar n) e| ξ = ExprVar (ξ n). Lemma ExprRenameVar : forall n ξ, (ExprVar n) e| ξ = ExprVar (ξ n).
...@@ -71,20 +68,17 @@ Module Type LocalLang. ...@@ -71,20 +68,17 @@ Module Type LocalLang.
Qed. Qed.
(* Renaming in an expression twice should behave (*
compositionally. For technical reasons, we need Renaming in an expression twice should behave compositionally. For technical reasons,
this to prove an important property of Pirouette. *) we need this to prove an important property of Pirouette.
*)
Parameter ExprRenameFusion : forall (e : Expr) (ξ1 ξ2 : nat -> nat), Parameter ExprRenameFusion : forall (e : Expr) (ξ1 ξ2 : nat -> nat),
(e e| ξ1) e| ξ2 = e e| fun n => ξ2 (ξ1 n). (e e| ξ1) e| ξ2 = e e| fun n => ξ2 (ξ1 n).
(* Parameter ExprSubstFusion : forall (e : Expr) (σ1 σ2 : nat -> Expr), *)
(* (e [e| σ1]) [e|σ2] = e [e| fun n => σ1 n [e| σ2]]. *)
(* (*
Substitution must be _extensional_ in the sense Substitution must be _extensional_ in the sense that it does not rely on the
that it does not rely on the implementation of implementation of the substitution functions. This allows us to show that renaming is
the substitution functions. This allows us to show also extensional.
that renaming is also extensional.
*) *)
Parameter ExprSubstExt : forall (e : Expr) (σ1 σ2 : nat -> Expr), Parameter ExprSubstExt : forall (e : Expr) (σ1 σ2 : nat -> Expr),
(forall n, σ1 n = σ2 n) -> e [e| σ1] = e [e| σ2]. (forall n, σ1 n = σ2 n) -> e [e| σ1] = e [e| σ2].
...@@ -97,10 +91,8 @@ Module Type LocalLang. ...@@ -97,10 +91,8 @@ Module Type LocalLang.
Qed. Qed.
(* (*
We define identity substitution and renamings. We define identity substitution and renamings. We require that the substitution behave
We require that the substitution behave as an as an identity. From that, we can show that the renaming also behaves as an identity.
identity. From that, we can show that the renaming
also behaves as an identity.
*) *)
Definition ExprIdSubst : nat -> Expr := fun n => ExprVar n. Definition ExprIdSubst : nat -> Expr := fun n => ExprVar n.
Parameter ExprIdentitySubstSpec : forall (e : Expr), e [e| ExprIdSubst] = e. Parameter ExprIdentitySubstSpec : forall (e : Expr), e [e| ExprIdSubst] = e.
...@@ -110,19 +102,15 @@ Module Type LocalLang. ...@@ -110,19 +102,15 @@ Module Type LocalLang.
intros e; rewrite ExprRenameSpec; unfold ExprIdRenaming; cbn. intros e; rewrite ExprRenameSpec; unfold ExprIdRenaming; cbn.
apply ExprIdentitySubstSpec. apply ExprIdentitySubstSpec.
Qed. Qed.
(* (*
Substitution with de Bruijn indices usually relies Substitution with de Bruijn indices usually relies on `up` constructions on
on `up` constructions on substitutions. These substitutions. These are used when going past a constructor to ensure that counting is
are used when going past a constructor to ensure done correctly.
that counting is done correctly.
Since we don't define substitution explicitly here, nor do we have binders, these
Since we don't define substitution explicitly aren't used here. However, we define them for convenience's sake. We also prove that
here, nor do we have binders, these aren't used here. they do not affect the identity substitution and renaming.
However, we define them for convenience's sake.
We also prove that they do not affect the
identity substitution and renaming.
*) *)
Definition ExprUpSubst : (nat -> Expr) -> nat -> Expr := Definition ExprUpSubst : (nat -> Expr) -> nat -> Expr :=
fun σ n => fun σ n =>
...@@ -161,29 +149,26 @@ Module Type LocalLang. ...@@ -161,29 +149,26 @@ Module Type LocalLang.
Qed. Qed.
(* (*
We require separate boolean expressions `true` and `false`. We require separate boolean expressions `true` and `false`. These must be separate
These must be separate expressions, and both be values. expressions, and both be values.
*) *)
Parameter tt ff : Expr. Parameter tt ff : Expr.
Parameter ttValue : ExprVal tt. Parameter ttValue : ExprVal tt.
Parameter ffValue : ExprVal ff. Parameter ffValue : ExprVal ff.
Parameter boolSeperation : tt <> ff. Parameter boolSeperation : tt <> ff.
(* (*
ExprStep is the small-step semantics for the ExprStep is the small-step semantics for the local language. We require that values not
local language. We require that values not be be able to take a step, which reflects the fact that we are using _small_-step
able to take a step, which reflects the fact that semantics.
we are using _small_-step semantics.
*) *)
Parameter ExprStep : Expr -> Expr -> Prop. Parameter ExprStep : Expr -> Expr -> Prop.
Parameter NoExprStepFromVal : forall v, ExprVal v -> forall e, ~ ExprStep v e. Parameter NoExprStepFromVal : forall v, ExprVal v -> forall e, ~ ExprStep v e.
(* (*
Substitution, renaming, and stepping Substitution, renaming, and stepping should not change the fact that expressions are
should not change the fact that closed above some level.
expressions are closed above some level.
*) *)
Parameter ExprRenameClosedAbove : forall e n ξ m, Parameter ExprRenameClosedAbove : forall e n ξ m,
(forall k, k < n -> ξ k < m) -> (forall k, k < n -> ξ k < m) ->
......
Require Export LocalLang. Require Export LocalLang.
Require Export TypedLocalLang. Require Export TypedLocalLang.
Module Type SoundlyTypedLocalLang (E : LocalLang) (TE : TypedLocalLang E). Module Type SoundlyTypedLocalLang (Import LL : LocalLang) (Import TLL : TypedLocalLang LL).
Import E.
Import TE.
(*
A soundly-typed local language does not allow boolean values other than true and false.
This is important in order to know that if expressions in Pirouette don't go wrong. If
we didn't have this, we could have a boolean expression which can't reduce, yet is
neither true nor false.
*)
Parameter BoolInversion : forall (Γ : nat -> ExprTyp) (v : Expr), Parameter BoolInversion : forall (Γ : nat -> ExprTyp) (v : Expr),
Γ e v ::: bool -> Γ e v ::: bool ->
ExprVal v -> ExprVal v ->
{v = tt} + {v = ff}. {v = tt} + {v = ff}.
(*
Progress and preservation for the local language is standard.
*)
Parameter ExprPreservation : forall (Γ : nat -> ExprTyp) (e1 e2 : Expr) (τ : ExprTyp), Parameter ExprPreservation : forall (Γ : nat -> ExprTyp) (e1 e2 : Expr) (τ : ExprTyp),
Γ e e1 ::: τ -> ExprStep e1 e2 -> Γ e e2 ::: τ. Γ e e1 ::: τ -> ExprStep e1 e2 -> Γ e e2 ::: τ.
Parameter ExprProgress : forall (Γ : nat -> ExprTyp) (e1 : Expr) (τ : ExprTyp), Parameter ExprProgress : forall (Γ : nat -> ExprTyp) (e1 : Expr) (τ : ExprTyp),
......
Require Export LocalLang. Require Export LocalLang.
Module Type TypedLocalLang (E : LocalLang). (*
Import E. Assumptions for a type system for local languages.
Again, this is given as a module type. See STLC.v and TypedNatLang.v for instantiations.
*)
Module Type TypedLocalLang (Import E : LocalLang).
(*
Types are a Set with decidable equality.
*)
Parameter ExprTyp : Set. Parameter ExprTyp : Set.
Parameter ExprTypEqDec : forall tau sigma : ExprTyp, {tau = sigma} + {tau <> sigma}. Parameter ExprTypEqDec : forall tau sigma : ExprTyp, {tau = sigma} + {tau <> sigma}.
(*
We require a typing judgment of the form Γ e : τ. We represent a context Γ as a
function from natural numbers (which represent variables) to types. This judgment is a
proposition (probably given as an inductive type, but we do not bake that in).
*)
Parameter ExprTyping : (nat -> ExprTyp) -> Expr -> ExprTyp -> Prop. Parameter ExprTyping : (nat -> ExprTyp) -> Expr -> ExprTyp -> Prop.
Notation "Gamma ⊢e e ::: tau" := (ExprTyping Gamma e tau) (at level 30). Notation "Gamma ⊢e e ::: tau" := (ExprTyping Gamma e tau) (at level 30).
(*
Variables are given the type they are assigned in the context.
*)
Parameter ExprVarTyping : forall (Γ : nat -> ExprTyp) (n : nat), Parameter ExprVarTyping : forall (Γ : nat -> ExprTyp) (n : nat),
Γ e (ExprVar n) ::: (Γ n). Γ e (ExprVar n) ::: (Γ n).
(*
Typing is extensional in the since that it does not look at the internal definition of
its context; it only cares about what type the context associates with what variable.
*)
Parameter ExprTypingExt : forall (Γ Δ : nat -> ExprTyp) (e : Expr) (τ : ExprTyp), Parameter ExprTypingExt : forall (Γ Δ : nat -> ExprTyp) (e : Expr) (τ : ExprTyp),
(forall n, Γ n = Δ n) -> (forall n, Γ n = Δ n) ->
Γ e e ::: τ -> Γ e e ::: τ ->
Δ e e ::: τ. Δ e e ::: τ.
(*
We require that each expression have a unique type within a given context. This is
probably the most burdensome requirement of this module type. However, it is necessary
for equivalence of choreographies to be type preserving.
*)
Parameter ExprTypingUnique : forall (Γ : nat -> ExprTyp) (e : Expr) (τ σ : ExprTyp), Parameter ExprTypingUnique : forall (Γ : nat -> ExprTyp) (e : Expr) (τ σ : ExprTyp),
Γ e e ::: τ -> Γ e e ::: τ ->
Γ e e ::: σ -> Γ e e ::: σ ->
τ = σ. τ = σ.
Parameter ExprWeakening : forall (Γ Δ : nat -> ExprTyp) (ξ : nat -> nat) (e : Expr) (τ : ExprTyp), (*
(forall n, Γ n = Δ (ξ n)) -> The type system should not take the values assigned by the context to variables not
Γ e e ::: τ -> free in the expression. Thus, if an expression e is closed above n, the values of the
Δ e e e| ξ⟩ ::: τ. context above n should not matter.
This is enough to allow us to prove that the context does not matter at all when typing
closed programs. Since we insist that all values are closed, it does not matter when
typing values.
*)
Parameter ExprClosedAboveTyping : forall (Γ Δ : nat -> ExprTyp) (e : Expr) (τ : ExprTyp) (n : nat), Parameter ExprClosedAboveTyping : forall (Γ Δ : nat -> ExprTyp) (e : Expr) (τ : ExprTyp) (n : nat),
ExprClosedAbove n e -> (forall m, m < n -> Γ m = Δ m) -> Γ e e ::: τ -> Δ e e ::: τ. ExprClosedAbove n e -> (forall m, m < n -> Γ m = Δ m) -> Γ e e ::: τ -> Δ e e ::: τ.
Lemma ExprClosedTyping : forall (Γ Δ : nat -> ExprTyp) (e : Expr) (τ : ExprTyp), Lemma ExprClosedTyping : forall (Γ Δ : nat -> ExprTyp) (e : Expr) (τ : ExprTyp),
...@@ -43,56 +72,89 @@ Module Type TypedLocalLang (E : LocalLang). ...@@ -43,56 +72,89 @@ Module Type TypedLocalLang (E : LocalLang).
apply ExprValuesClosed; auto. apply ExprValuesClosed; auto.
Qed. Qed.
(*
We represent weakening by allowing renaming, changing the context to match. This
represents exchange as well as the classical definition of weakening. To see why this
represents weakening, consider an expression e which is closed above n, but which does
contain the variable n. If we type e in some context Γ, we can think of the "real"
finite context as Γ up through n. Then imagine renaming with the function
ξ i = if i = n + 1 then 0 else i + 1
Clearly, the resulting expression is only closed above n + 1. Thus, the new real
context contains some variables not in the original context.
*)
Parameter ExprWeakening : forall (Γ Δ : nat -> ExprTyp) (ξ : nat -> nat) (e : Expr) (τ : ExprTyp),
(forall n, Γ n = Δ (ξ n)) ->
Γ e e ::: τ ->
Δ e e e| ξ⟩ ::: τ.
(*
We require a type of booleans, and require that true and false are of boolean type.
*)
Parameter bool : ExprTyp. Parameter bool : ExprTyp.
Parameter TrueTyping : forall (Γ : nat -> ExprTyp), Parameter TrueTyping : forall (Γ : nat -> ExprTyp),
Γ e tt ::: bool. Γ e tt ::: bool.
Parameter FalseTyping : forall (Γ : nat -> ExprTyp), Parameter FalseTyping : forall (Γ : nat -> ExprTyp),
Γ e ff ::: bool. Γ e ff ::: bool.
(*
Substitutions replace every variable with a new expression. These expressions can
themselves contain variables. If Γ is a context, and σ assigns every variable x an
expression that (under a new context Δ) has the type Γ gives x, then we say that σ
changes Γ to Δ, which we write Γ σ Δ.
*)
Definition ExprSubstTyping : (nat -> ExprTyp) -> (nat -> Expr) -> (nat -> ExprTyp) -> Prop := Definition ExprSubstTyping : (nat -> ExprTyp) -> (nat -> Expr) -> (nat -> ExprTyp) -> Prop :=
fun Γ σ Δ => forall n : nat, Δ e (σ n) ::: (Γ n). fun Γ σ Δ => forall n : nat, Δ e (σ n) ::: (Γ n).
Notation "Gamma ⊢es sigma ⊣ Delta" := (ExprSubstTyping Gamma sigma Delta) (at level 30). Notation "Gamma ⊢es sigma ⊣ Delta" := (ExprSubstTyping Gamma sigma Delta) (at level 30).
(*
We then require that, if σ changes Γ to Δ and e hastype τ under Γ, then e[e| σ] has
type τ under Δ.
*)
Parameter ExprSubstType : Parameter ExprSubstType :
forall (Γ Δ : nat -> ExprTyp) (sigma : nat -> Expr) (e : Expr) (τ : ExprTyp), forall (Γ Δ : nat -> ExprTyp) (σ : nat -> Expr) (e : Expr) (τ : ExprTyp),
Γ es sigma Δ -> Γ e e ::: τ -> Δ e e [e| sigma ] ::: τ. Γ es σ Δ -> Γ e e ::: τ -> Δ e e [e| σ ] ::: τ.
(*
Clearly, the identity substitution changes Γ to itself.
*)
Lemma ExprIdSubstTyping : forall (Γ : nat -> ExprTyp), Γ es ExprIdSubst Γ. Lemma ExprIdSubstTyping : forall (Γ : nat -> ExprTyp), Γ es ExprIdSubst Γ.
Proof. Proof.
unfold ExprSubstTyping. intros Γ n. unfold ExprIdSubst. apply ExprVarTyping. unfold ExprSubstTyping; intros Γ n; unfold ExprIdSubst; apply ExprVarTyping.
Qed. Qed.
Lemma ExprSubstLWeakening : forall (Γ Δ1 Δ2 : nat -> ExprTyp) (σ : nat -> Expr) (ξ : nat -> nat), (* Lemma ExprSubstLWeakening : forall (Γ Δ1 Δ2 : nat -> ExprTyp) (σ : nat -> Expr) (ξ : nat -> nat), *)
(forall n, Δ1 n = Δ2 (ξ n)) -> (* (forall n, Δ1 n = Δ2 (ξ n)) -> *)
Γ es σ Δ1 -> (* Γ es σ Δ1 -> *)
Γ es fun n => (σ n) e|ξ⟩ Δ2. (* Γ es fun n => (σ n) e|ξ⟩ Δ2. *)
Proof. (* Proof. *)
intros Γ Δ1 Δ2 σ ξ subΔ typing. (* intros Γ Δ1 Δ2 σ ξ subΔ typing. *)
unfold ExprSubstTyping in *; intro n. (* unfold ExprSubstTyping in *; intro n. *)
eapply ExprWeakening; eauto. (* eapply ExprWeakening; eauto. *)
Qed. (* Qed. *)
Lemma ExprSubstRWeakening : forall (Γ1 Γ2 Δ : nat -> ExprTyp) (σ : nat -> Expr) (ξ : nat -> nat), (* Lemma ExprSubstRWeakening : forall (Γ1 Γ2 Δ : nat -> ExprTyp) (σ : nat -> Expr) (ξ : nat -> nat), *)
(forall n, Γ1 (ξ n) = Γ2 n) -> (* (forall n, Γ1 (ξ n) = Γ2 n) -> *)
Γ1 es σ Δ -> (* Γ1 es σ Δ -> *)
Γ2 es fun n => σ (ξ n) Δ. (* Γ2 es fun n => σ (ξ n) Δ. *)
Proof. (* Proof. *)
intros Γ1 Γ2 Δ σ ξ subΓ typing. (* intros Γ1 Γ2 Δ σ ξ subΓ typing. *)
unfold ExprSubstTyping in *; intro n. (* unfold ExprSubstTyping in *; intro n. *)
rewrite <- subΓ. apply typing. (* rewrite <- subΓ. apply typing. *)
Qed. (* Qed. *)
Lemma ExprSubstTypeExpand : forall (Γ Δ : nat -> ExprTyp) (σ : nat -> Expr), (* Lemma ExprSubstTypeExpand : forall (Γ Δ : nat -> ExprTyp) (σ : nat -> Expr), *)
Γ es σ Δ -> (* Γ es σ Δ -> *)
forall τ : ExprTyp, ExprSubstTyping (fun n => match n with | 0 => τ | S n => Γ n end) (* forall τ : ExprTyp, ExprSubstTyping (fun n => match n with | 0 => τ | S n => Γ n end) *)
(ExprUpSubst σ) (* (ExprUpSubst σ) *)
(fun n => match n with |0 => τ | S n => Δ n end). (* (fun n => match n with |0 => τ | S n => Δ n end). *)
Proof. (* Proof. *)
intros Γ Δ σ typing τ. (* intros Γ Δ σ typing τ. *)
unfold ExprUpSubst. (* unfold ExprUpSubst. *)
unfold ExprSubstTyping in *. (* unfold ExprSubstTyping in *. *)
intro m. (* intro m. *)
unfold ExprUpSubst. destruct m; simpl. (* unfold ExprUpSubst. destruct m; simpl. *)
apply ExprVarTyping. (* apply ExprVarTyping. *)
apply ExprWeakening with (Γ := Δ); auto. (* apply ExprWeakening with (Γ := Δ); auto. *)
Qed. (* Qed. *)
End TypedLocalLang. End TypedLocalLang.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment