diff --git a/software_foundations.ipkg b/software_foundations.ipkg index b94469b..9b4518a 100644 --- a/software_foundations.ipkg +++ b/software_foundations.ipkg @@ -12,6 +12,7 @@ modules = Basics , Rel , Imp , ImpParser + , Smallstep brief = "Software Foundations in Idris" version = 0.0.1.0 diff --git a/src/Maps.lidr b/src/Maps.lidr index eb4bf08..6aeba8f 100644 --- a/src/Maps.lidr +++ b/src/Maps.lidr @@ -63,6 +63,14 @@ equality comparison function for \idr{Id} and its fundamental property. > beq_id (MkId n1) (MkId n2) = decAsBool $ decEq n1 n2 > +> idInjective : {x,y : String} -> (MkId x = MkId y) -> x = y +> idInjective Refl = Refl + +> implementation DecEq Id where +> decEq (MkId s1) (MkId s2) with (decEq s1 s2) +> | Yes prf = Yes (cong prf) +> | No contra = No (\h : MkId s1 = MkId s2 => contra (idInjective h)) + \todo[inline]{Edit} (The function \idr{decEq} comes from Idris's string library. If you check its diff --git a/src/Smallstep.lidr b/src/Smallstep.lidr new file mode 100644 index 0000000..d89c17b --- /dev/null +++ b/src/Smallstep.lidr @@ -0,0 +1,1479 @@ += Library Smallstep + +== Smallstep: Small-step Operational Semantics + +> module Smallstep +> +> import Maps +> import Imp +> +> %hide Language.Reflection.P +> +> %access public export +> %default total +> + +The evaluators we have seen so far (for `aexp`s, `bexp`s, commands, ...) have +been formulated in a "big-step" style: they specify how a given expression can +be evaluated to its final value (or a command plus a store to a final store) +"all in one big step." + +This style is simple and natural for many purposes -- indeed, Gilles Kahn, who +popularized it, called it _natural semantics_. But there are some things it does +not do well. In particular, it does not give us a natural way of talking about +_concurrent_ programming languages, where the semantics of a program -- i.e., +the essence of how it behaves -- is not just which input states get mapped to +which output states, but also includes the intermediate states that it passes +through along the way, since these states can also be observed by concurrently +executing code. + +Another shortcoming of the big-step style is more technical, but critical in +many situations. Suppose we want to define a variant of Imp where variables +could hold _either_ numbers _or_ lists of numbers. In the syntax of this +extended language, it will be possible to write strange expressions like `2 + +nil`, and our semantics for arithmetic expressions will then need to say +something about how such expressions behave. One possibility is to maintain the +convention that every arithmetic expressions evaluates to some number by +choosing some way of viewing a list as a number -- e.g., by specifying that a +list should be interpreted as `0` when it occurs in a context expecting a +number. But this is really a bit of a hack. + +A much more natural approach is simply to say that the behavior of an expression +like `2+nil` is _undefined_ -- i.e., it doesn't evaluate to any result at all. +And we can easily do this: we just have to formulate `aeval` and `beval` as +`Inductive` propositions rather than Fixpoints, so that we can make them partial +functions instead of total ones. + +Now, however, we encounter a serious deficiency. In this language, a command +might fail to map a given starting state to any ending state for _two quite +different reasons_: either because the execution gets into an infinite loop or +because, at some point, the program tries to do an operation that makes no +sense, such as adding a number to a list, so that none of the evaluation rules +can be applied. + +These two outcomes -- nontermination vs. getting stuck in an erroneous +configuration -- should not be confused. In particular, we want to _allow_ the +first (permitting the possibility of infinite loops is the price we pay for the +convenience of programming with general looping constructs like `while`) but +_prevent_ the second (which is just wrong), for example by adding some form of +_typechecking_ to the language. Indeed, this will be a major topic for the rest +of the course. As a first step, we need a way of presenting the semantics that +allows us to distinguish nontermination from erroneous "stuck states." + +So, for lots of reasons, we'd often like to have a finer-grained way of defining +and reasoning about program behaviors. This is the topic of the present chapter. +Our goal is to replace the "big-step" `eval` relation with a "small-step" +relation that specifies, for a given program, how the "atomic steps" of +computation are performed. + +== A Toy Language + +To save space in the discussion, let's go back to an incredibly simple language +containing just constants and addition. (We use single letters -- `C` and `P` +(for Constant and Plus) -- as constructor names, for brevity.) At the end of the +chapter, we'll see how to apply the same techniques to the full Imp language. + +> data Tm : Type where +> C : Nat -> Tm -- Constant +> P : Tm -> Tm -> Tm -- Plus +> + +Here is a standard evaluator for this language, written in the big-step style +that we've been using up to this point. + +> evalF : (t : Tm) -> Nat +> evalF (C n) = n +> evalF (P a1 a2) = evalF a1 + evalF a2 +> + +Here is the same evaluator, written in exactly the same style, but formulated as +an inductively defined relation. Again, we use the notation `t >>> n` for "`t` +evaluates to `n`." + +\[ + \begin{prooftree} + \infer0[\idr{E_Const}]{\idr{C n >>> n}} + \end{prooftree} + \newline +\] + +\[ + \begin{prooftree} + \hypo{\idr{t1 >>> n1}} + \hypo{\idr{t1 >>> n2}} + \infer2[\idr{E_Plus}]{\idr{P t1 t2 >>> n1 + n2}} + \end{prooftree} +\] + +> infixl 6 >>> +> +> mutual +> (>>>) : Tm -> Nat -> Type +> (>>>) = Eval +> +> data Eval : Tm -> Nat -> Type where +> E_Const : C n >>> n +> E_Plus : t1 >>> n1 -> t2 >>> n2 -> P t1 t2 >>> n1 + n2 +> + +Now, here is the corresponding _small-step_ evaluation relation. + +\[ + \begin{prooftree} + \infer0[\idr{ST_PlusConstConst'}]{\idr{P (C n1) (C n2) ->> C (n1 + n2)}} + \end{prooftree} +\] + +\[ + \begin{prooftree} + \hypo{\idr{t1 ->> t1'}} + \infer1[\idr{ST_Plus1'}]{\idr{P t1 t2 ->> P t1' t2}} + \end{prooftree} +\] + +\[ + \begin{prooftree} + \hypo{\idr{t2 ->> t2'}} + \infer1[\idr{ST_Plus2'}]{\idr{P (C n1) t2 ->> P (C n1) t2'}} + \end{prooftree} +\] + +> mutual +> infixl 6 ->> +> (->>) : Tm -> Tm -> Type +> (->>) = Step' +> +> data Step' : Tm -> Tm -> Type where +> ST_PlusConstConst' : P (C n1) (C n2) ->> C (n1 + n2) +> ST_Plus1' : t1 ->> t1' -> P t1 t2 ->> P t1' t2 +> ST_Plus2' : t2 ->> t2' -> P (C n1) t2 ->> P (C n1) t2' +> + +Things to notice: + +- We are defining just a single reduction step, in which one `P` node is + replaced by its value. + +- Each step finds the _leftmost_ `P` node that is ready to go (both of its + operands are constants) and rewrites it in place. The first rule tells how to + rewrite this `P` node itself; the other two rules tell how to find it. + +- A term that is just a constant cannot take a step. + +Let's pause and check a couple of examples of reasoning with the `step` +relation... + +If `t1` can take a step to `t1'`, then `P t1 t2` steps to `P t1' t2`: + +> test_step_1 : +> P +> (P (C 0) (C 3)) +> (P (C 2) (C 4)) +> ->> +> P +> (C (0 + 3)) +> (P (C 2) (C 4)) +> test_step_1 = ST_Plus1' ST_PlusConstConst' +> + + +==== Exercise: 1 star (test_step_2) + +Right-hand sides of sums can take a step only when the left-hand side is +finished: if `t2` can take a step to `t2'`, then `P (C n) t2` steps to `P (C n) +t2'`: + +> test_step_2 : +> P +> (C 0) +> (P +> (C 2) +> (P (C 0) (C 3))) +> ->> +> P +> (C 0) +> (P +> (C 2) +> (C (0 + 3))) +> test_step_2 = ?test_step_2_rhs +> + +$\square$ + + +== Relations + +We will be working with several different single-step relations, so it is +helpful to generalize a bit and state a few definitions and theorems about +relations in general. (The optional chapter `Rel.lidr` develops some of these +ideas in a bit more detail; it may be useful if the treatment here is too dense. + +A _binary relation_ on a set `X` is a family of propositions parameterized by +two elements of `X` -- i.e., a proposition about pairs of elements of `X`. + +> Relation : Type -> Type +> Relation t = t -> t -> Type +> + +Our main examples of such relations in this chapter will be the single-step +reduction relation, `->>`, and its multi-step variant, `->>*` (defined below), +but there are many other examples -- e.g., the "equals," "less than," "less than +or equal to," and "is the square of" relations on numbers, and the "prefix of" +relation on lists and strings. + +One simple property of the `->>` relation is that, like the big-step evaluation +relation for Imp, it is _deterministic_. + +_Theorem_: For each `t`, there is at most one `t'` such that `t` steps to `t'` +(`t ->> t'` is provable). This is the same as saying that `->>` is +deterministic. + +_Proof sketch_: We show that if `x` steps to both `y1` and `y2`, then `y1` and +`y2` are equal, by induction on a derivation of `step x y1`. There are several +cases to consider, depending on the last rule used in this derivation and the +last rule in the given derivation of `step x y2`. + +- If both are `ST_PlusConstConst'`, the result is immediate. + +- The cases when both derivations end with `ST_Plus1` or `ST_Plus2` follow by + the induction hypothesis. + +- It cannot happen that one is `ST_PlusConstConst'` and the other is `ST_Plus1` + or `ST_Plus2'`, since this would imply that `x` has the form `P t1 t2` where + both `t1` and `t2` are constants (by `ST_PlusConstConst'`) _and_ one of `t1` + or `t2` has the form `P _`. + +- Similarly, it cannot happen that one is `ST_Plus1'` and the other is + `ST_Plus2'`, since this would imply that `x` has the form `P t1 t2` where `t1` + has both the form `P t11 t12` and the form `C n`. + +Formally: + +> Uninhabited (Step' (C _) _) where +> uninhabited ST_PlusConstConst' impossible +> uninhabited (ST_Plus1' _) impossible +> uninhabited (ST_Plus2' _) impossible +> +> deterministic : {xt : Type} -> (r : Relation xt) -> Type +> deterministic {xt} r = {x : xt} -> {y1 : xt} -> {y2 : xt} +> -> r x y1 -> r x y2 -> y1 = y2 +> +> step_deterministic : deterministic Step' +> step_deterministic ST_PlusConstConst' ST_PlusConstConst' = Refl +> step_deterministic ST_PlusConstConst' (ST_Plus1' s2) = absurd s2 +> step_deterministic ST_PlusConstConst' (ST_Plus2' s2) = absurd s2 +> step_deterministic (ST_Plus1' s1) ST_PlusConstConst' = absurd s1 +> step_deterministic (ST_Plus1' s1) (ST_Plus1' s2) = +> rewrite step_deterministic s1 s2 in Refl +> step_deterministic (ST_Plus1' s1) (ST_Plus2' s2) = absurd s1 +> step_deterministic (ST_Plus2' s1) ST_PlusConstConst' = absurd s1 +> step_deterministic (ST_Plus2' s1) (ST_Plus1' s2) = absurd s2 +> step_deterministic (ST_Plus2' s1) (ST_Plus2' s2) = +> rewrite step_deterministic s1 s2 in Refl +> + +\todo[inline]{Matching on implicit shortens the proof} + +> step_deterministic_2 : deterministic Step' +> step_deterministic_2 {x=P (C _) (C _)} ST_PlusConstConst' ST_PlusConstConst' = +> Refl +> step_deterministic_2 {x=P _ _} (ST_Plus1' s1) (ST_Plus1' s2) = +> rewrite step_deterministic_2 s1 s2 in Refl +> step_deterministic_2 {x=P (C _) _} (ST_Plus2' s1) (ST_Plus1' s2) = +> absurd s2 +> step_deterministic_2 {x=P (C _) _} (ST_Plus2' s1) (ST_Plus2' s2) = +> rewrite step_deterministic_2 s1 s2 in Refl +> + + +=== Values + +Next, it will be useful to slightly reformulate the definition of single-step +reduction by stating it in terms of "values." + +It is useful to think of the `->>` relation as defining an _abstract machine_: + +- At any moment, the _state_ of the machine is a term. + +- A _step_ of the machine is an atomic unit of computation -- here, a single + "add" operation. + +- The _halting states_ of the machine are ones where there is no more + computation to be done. + +We can then execute a term `t` as follows: + +- Take `t` as the starting state of the machine. + +- Repeatedly use the `->>` relation to find a sequence of machine states, + starting with `t`, where each state steps to the next. + +- When no more reduction is possible, "read out" the final state of the machine + as the result of execution. + +Intuitively, it is clear that the final states of the machine are always terms +of the form `C n` for some `n`. We call such terms _values_. + +> data Value : Tm -> Type where +> V_const : (n : Nat) -> Value (C n) +> +> Uninhabited (Value (P _ _)) where +> uninhabited V_const impossible +> + +Having introduced the idea of values, we can use it in the definition of the +`>>-` relation to write `ST_Plus2` rule in a slightly more elegant way: + + +\[ + \begin{prooftree} + \infer0[\idr{ST_PlusConstConst}]{\idr{P (C n1) (C n2) >>- C (n1 + n2)}} + \end{prooftree} +\] + +\[ + \begin{prooftree} + \hypo{\idr{t1 >>- t1'}} + \infer1[\idr{ST_Plus1}]{\idr{P t1 t2 >>- P t1' t2}} + \end{prooftree} +\] + +\[ + \begin{prooftree} + \hypo{\idr{value v1}} + \hypo{\idr{t2 >>- t2'}} + \infer2[\idr{ST_Plus2}]{\idr{P v1 t2 >>- P v1 t2'}} + \end{prooftree} +\] + +Again, the variable names here carry important information: by convention, `v1` +ranges only over values, while `t1` and `t2` range over arbitrary terms. (Given +this convention, the explicit `value` hypothesis is arguably redundant. We'll +keep it for now, to maintain a close correspondence between the informal and +Idris versions of the rules, but later on we'll drop it in informal rules for +brevity.) + +Here are the formal rules: + +> mutual +> infixl 6 >>- +> (>>-) : Tm -> Tm -> Type +> (>>-) = Step +> +> data Step : Tm -> Tm -> Type where +> ST_PlusConstConst : P (C n1) (C n2) >>- C (n1 + n2) +> ST_Plus1 : t1 >>- t1' -> P t1 t2 >>- P t1' t2 +> ST_Plus2 : Value v1 -> t2 >>- t2' -> P v1 t2 >>- P v1 t2' +> + +==== Exercise: 3 stars, recommended (redo_determinism) + +As a sanity check on this change, let's re-verify determinism. + +_Proof sketch_: We must show that if `x` steps to both `y1` and `y2`, then `y1` +and `y2` are equal. Consider the final rules used in the derivations of `step x +y1` and `step x y2`. + +- If both are `ST_PlusConstConst`, the result is immediate. + +- It cannot happen that one is `ST_PlusConstConst` and the other is `ST_Plus1` + or `ST_Plus2`, since this would imply that `x` has the form `P t1 t2` where + both `t1` and `t2` are constants (by `ST_PlusConstConst`) _and_ one of `t1` or + `t2` has the form `P _`. + +- Similarly, it cannot happen that one is `ST_Plus1` and the other is + `ST_Plus2`, since this would imply that `x` has the form `P t1 t2` where `t1` + both has the form `P t11 t12` and is a value (hence has the form `C n`). + +- The cases when both derivations end with `ST_Plus1` or `ST_Plus2` follow by + the induction hypothesis. + +Most of this proof is the same as the one above. But to get maximum benefit from +the exercise you should try to write your formal version from scratch and just +use the earlier one if you get stuck. + +> Uninhabited (Step (C _) _) where +> uninhabited ST_PlusConstConst impossible +> uninhabited (ST_Plus1 _) impossible +> uninhabited (ST_Plus2 _ _) impossible +> +> step_deterministic' : deterministic Step +> step_deterministic' = ?step_deterministic_rhs +> + +$\square$ + + +=== Strong Progress and Normal Forms + +The definition of single-step reduction for our toy language is fairly simple, +but for a larger language it would be easy to forget one of the rules and +accidentally create a situation where some term cannot take a step even though +it has not been completely reduced to a value. The following theorem shows that +we did not, in fact, make such a mistake here. + +_Theorem_ (_Strong Progress_): If `t` is a term, then either `t` is a value or +else there exists a term `t'` such that `t >>- t'`. + +_Proof_: By induction on `t`. + +- Suppose `t = C n`. Then `t` is a value. + +- Suppose `t = P t1 t2`, where (by the IH) `t1` either is a value or can step to +some `t1'`, and where `t2` is either a value or can step to some `t2'`. We must +show `P t1 t2` is either a value or steps to some `t'`. + + - If `t1` and `t2` are both values, then `t` can take a step, by + `ST_PlusConstConst`. + + - If `t1` is a value and `t2` can take a step, then so can `t`, by `ST_Plus2`. + + - If `t1` can take a step, then so can `t`, by `ST_Plus1`. + +Or, formally: + +> strong_progress : (t : Tm) -> Either (Value t) (t' : Tm ** Step t t') +> strong_progress (C n) = Left (V_const n) +> strong_progress (P (C n) (C n')) = Right (C (n + n') ** ST_PlusConstConst) +> strong_progress (P (C n) (P l r)) = +> case strong_progress (P l r) of +> Right (r' ** prf) => Right (P (C n) r' ** ST_Plus2 (V_const n) prf) +> Left (V_const (P _ _)) impossible +> strong_progress (P (P l r) r') = +> case strong_progress (P l r) of +> Right (l' ** prf) => Right (P l' r' ** ST_Plus1 prf) +> Left (V_const (P _ _)) impossible +> + +This important property is called _strong progress_, because every term either +is a value or can "make progress" by stepping to some other term. (The +qualifier "strong" distinguishes it from a more refined version that we'll see +in later chapters, called just _progress_.) + +The idea of "making progress" can be extended to tell us something interesting +about values: in this language, values are exactly the terms that _cannot_ make +progress in this sense. + +To state this observation formally, let's begin by giving a name to terms that +cannot make progress. We'll call them _normal forms_. + +> normal_form : {t : Type} -> Relation t -> t -> Type +> normal_form r x = Not (x' ** r x x') +> + +Note that this definition specifies what it is to be a normal form for an +_arbitrary_ relation `R` over an arbitrary set `X`, not just for the particular +single-step reduction relation over terms that we are interested in at the +moment. We'll re-use the same terminology for talking about other relations +later in the course. + +We can use this terminology to generalize the observation we made in the strong +progress theorem: in this language, normal forms and values are actually the +same thing. + +> value_is_nf : (v : Tm) -> Value v -> normal_form Step v +> value_is_nf (C n) prf = \(_ ** step) => uninhabited step +> value_is_nf (P l r) prf = absurd prf +> +> nf_is_value : (v : Tm) -> normal_form Step v -> Value v +> nf_is_value (C n) prf = V_const n +> nf_is_value (P l r) prf = +> case strong_progress (P l r) of +> Left va => va +> Right pa => void (prf pa) +> +> iff : (p, q : Type) -> Type -- TODO copied from "Logic.lidr" +> iff p q = (p -> q, q -> p) +> +> infixl 9 <-> +> (<->) : (p : Type) -> (q : Type) -> Type +> (<->) = iff +> +> nf_same_as_value : (normal_form Step t) <-> (Value t) +> nf_same_as_value {t} = (nf_is_value t, value_is_nf t) +> + +Why is this interesting? + +Because `value` is a syntactic concept -- it is defined by looking at the form +of a term -- while `normal_form` is a semantic one -- it is defined by looking +at how the term steps. It is not obvious that these concepts should coincide! + +Indeed, we could easily have written the definitions so that they would _not_ +coincide. + + +==== Exercise: 3 stars, optional (value_not_same_as_normal_form1) + +We might, for example, mistakenly define `value` so that it includes some terms +that are not finished reducing. + +(Even if you don't work this exercise and the following ones in Idris, make sure +you can think of an example of such a term.) + +> data Value' : Tm -> Type where +> V_const' : {n : Nat} -> Value' (C n) +> V_funny : {t1 : Tm} -> {n2 : Nat} -> Value' (P t1 (C n2)) +> +> mutual +> infixl 6 >>>- +> (>>>-) : Tm -> Tm -> Type +> (>>>-) = Step'' +> +> data Step'' : Tm -> Tm -> Type where +> ST_PlusConstConst'' : P (C n1) (C n2) >>>- C (n1 + n2) +> ST_Plus1'' : +> t1 >>>- t1' -> +> P t1 t2 >>>- P t1' t2 +> ST_Plus2'' : +> Value' v1 -> +> t2 >>>- t2' -> +> P v1 t2 >>>- P v1 t2' +> +> value_not_same_as_normal_form : (v : Tm ** (Value' v, Not (normal_form Step'' v))) +> value_not_same_as_normal_form = ?value_not_same_as_normal_form_rhs +> + +$\square$ + + +==== Exercise: 2 stars, optional (value_not_same_as_normal_form2) + +Alternatively, we might mistakenly define `step` so that it permits something +designated as a value to reduce further. + +> mutual +> infixl 6 ->>>- +> (->>>-) : Tm -> Tm -> Type +> (->>>-) = Step''' +> +> data Step''' : Tm -> Tm -> Type where +> ST_Funny : C n ->>>- P (C n) (C 0) +> ST_PlusConstConst''' : P (C n1) (C n2) ->>>- C (n1 + n2) +> ST_Plus1''' : +> t1 ->>>- t1' -> +> P t1 t2 ->>>- P t1' t2 +> ST_Plus2''' : +> Value' v1 -> +> t2 ->>>- t2' -> +> P v1 t2 ->>>- P v1 t2' +> +> value_not_same_as_normal_form''' : (v : Tm ** (Value v, Not (normal_form Step''' v))) +> value_not_same_as_normal_form''' = ?value_not_same_as_normal_form_rhs''' +> + +$\square$ + + +==== Exercise: 3 stars, optional (value_not_same_as_normal_form3) + +Finally, we might define `value` and `step` so that there is some term that is +not a value but that cannot take a step in the `step` relation. Such terms are +said to be _stuck_. In this case this is caused by a mistake in the semantics, +but we will also see situations where, even in a correct language definition, it +makes sense to allow some terms to be stuck. + +> mutual +> infixl 6 ->>- +> (->>-) : Tm -> Tm -> Type +> (->>-) = Step'''' +> +> data Step'''' : Tm -> Tm -> Type where +> ST_PlusConstConst'''' : P (C n1) (C n2) ->>- C (n1 + n2) +> ST_Plus1'''' : +> t1 ->>- t1' -> +> P t1 t2 ->>- P t1' t2 +> + +(Note that `ST_Plus2` is missing.) + +> value_not_same_as_normal_form'''' : (t : Tm ** (Not (Value t), normal_form Step'''' t)) +> value_not_same_as_normal_form'''' = ?value_not_same_as_normal_form_rhs'''' +> + +$\square$ + + +=== Additional Exercises + +Here is another very simple language whose terms, instead of being just addition +expressions and numbers, are just the booleans true and false and a conditional +expression... + +> data TmB : Type where +> Ttrue : TmB +> Tfalse : TmB +> Tif : TmB -> TmB -> TmB -> TmB +> +> data ValueB : TmB -> Type where +> V_true : ValueB Ttrue +> V_false : ValueB Tfalse +> +> mutual +> infixl 6 ->- +> (->-) : TmB -> TmB -> Type +> (->-) = StepB +> +> data StepB : TmB -> TmB -> Type where +> ST_IfTrue : Tif Ttrue t1 t2 ->- t1 +> ST_IfFalse : Tif Tfalse t1 t2 ->- t2 +> ST_If : t1 ->- t1' -> Tif t1 t2 t3 ->- Tif t1' t2 t3 +> + + +==== Exercise: 1 star (smallstep_bools) + +Which of the following propositions are provable? (This is just a thought +exercise, but for an extra challenge feel free to prove your answers in Idris.) + +> bool_step_prop1 : Tfalse ->- Tfalse +> bool_step_prop1 = ?bool_step_prop1_rhs +> +> bool_step_prop2 : +> Tif +> Ttrue +> (Tif Ttrue Ttrue Ttrue) +> (Tif Tfalse Tfalse Tfalse) +> ->- +> Ttrue +> bool_step_prop2 = ?bool_step_prop2_rhs +> +> bool_step_prop3 : +> Tif +> (Tif Ttrue Ttrue Ttrue) +> (Tif Ttrue Ttrue Ttrue) +> Tfalse +> ->- +> Tif +> Ttrue +> (Tif Ttrue Ttrue Ttrue) +> Tfalse +> bool_step_prop3 = ?bool_step_prop3_rhs +> + +$\square$ + + +==== Exercise: 3 stars, optional (progress_bool) + +Just as we proved a progress theorem for plus expressions, we can do so for +boolean expressions, as well. + +> strong_progressB : (t : TmB) -> Either (ValueB t) (t': TmB ** t ->- t') +> strong_progressB t = ?strong_progressB_rhs +> + + +==== Exercise: 2 stars, optional (step_deterministic) + +> step_deterministicB : deterministic StepB +> step_deterministicB = ?step_deterministicB_rhs +> + + +==== Exercise: 2 stars (smallstep_bool_shortcut) + +Suppose we want to add a "short circuit" to the step relation for boolean +expressions, so that it can recognize when the `then` and `else` branches of a +conditional are the same value (either `Ttrue` or `Tfalse`) and reduce the whole +conditional to this value in a single step, even if the guard has not yet been +reduced to a value. For example, we would like this proposition to be provable: + +```idris + Tif + (Tif Ttrue Ttrue Ttrue) + Tfalse + Tfalse + ->> + Tfalse +``` + +Write an extra clause for the step relation that achieves this effect and prove +`bool_step_prop4`. + +> mutual +> infixl 6 ->-> +> (->->) : TmB -> TmB -> Type +> (->->) = StepB' +> +> data StepB' : TmB -> TmB -> Type where +> ST_IfTrue' : Tif Ttrue t1 t2 ->-> t1 +> ST_IfFalse' : Tif Tfalse t1 t2 ->-> t2 +> ST_If' : t1 ->-> t1' -> Tif t1 t2 t3 ->-> Tif t1' t2 t3 +> -- FILL IN HERE +> +> bool_step_prop4 : Type +> bool_step_prop4 = +> Tif +> (Tif Ttrue Ttrue Ttrue) +> Tfalse +> Tfalse +> ->-> +> Tfalse +> +> bool_step_prop4_holds : Smallstep.bool_step_prop4 +> bool_step_prop4_holds = ?bool_step_prop4_holds_rhs +> + +$\square$ + + +==== Exercise: 3 stars, optional (properties_of_altered_step) + +It can be shown that the determinism and strong progress theorems for the step +relation in the lecture notes also hold for the definition of step given above. +After we add the clause `ST_ShortCircuit`... + +- Is the `step` relation still deterministic? Write yes or no and briefly (1 + sentence) explain your answer. + +Optional: prove your answer correct in Idris. + +- Does a strong progress theorem hold? Write yes or no and briefly (1 sentence) + explain your answer. + +Optional: prove your answer correct in Idris. + +In general, is there any way we could cause strong progress to fail if we took +away one or more constructors from the original step relation? Write yes or no +and briefly (1 sentence) explain your answer. + +$\square$ + + +== Multi-Step Reduction + +We've been working so far with the _single-step reduction_ relation `->>`, which +formalizes the individual steps of an abstract machine for executing programs. + +We can use the same machine to reduce programs to completion -- to find out what +final result they yield. This can be formalized as follows: + +- First, we define a _multi-step reduction relation_ `->>*`, which relates terms + `t` and `t'` if `t` can reach `t'` by any number (including zero) of single + reduction steps. + +- Then we define a "result" of a term `t` as a normal form that `t` can reach by + multi-step reduction. + +Since we'll want to reuse the idea of multi-step reduction many times, let's +take a little extra trouble and define it generically. + +Given a relation `r`, we define a relation `Multi r`, called the _multi-step +closure of `r`_ as follows. + +> data Multi : {t : Type} -> (r : Relation t) -> Relation t where +> Multi_refl : {x : t} -> Multi r x x +> Multi_step : {x, y, z : t} -> +> r x y -> Multi r y z -> Multi r x z +> +> infixl 6 ->>* +> (->>*) : Tm -> Tm -> Type +> (->>*) = Multi Step +> + +(In the `Rel` chapter of _Logical Foundations_ this relation is called +`clos_refl_trans_1n`. We give it a shorter name here for the sake of +readability.) + +The effect of this definition is that `Multi r` relates two elements `x` and `y` +if + +- `x = y`, or +- `r x y`, or +- there is some nonempty sequence `z1`, `z2`, ..., `zn` such that + + r x z1 + r z1 z2 + ... + r zn y. + +Thus, if `r` describes a single-step of computation, then `z1`...`zn` is the +sequence of intermediate steps of computation between `x` and `y`. + +We write `->>*` for the `Multi Step` relation on terms. + +The relation `Multi r` has several crucial properties. + +First, it is obviously _reflexive_ (that is, `forall x, Multi r x x`). In the +case of the `->>*` (i.e., `Multi Step`) relation, the intuition is that a term +can execute to itself by taking zero steps of execution. + +Second, it contains `r` -- that is, single-step executions are a particular case +of multi-step executions. (It is this fact that justifies the word "closure" in +the term "multi-step closure of `r`.") + +> multi_R : {t : Type} -> {r : Relation t} +> -> (x, y : t) -> r x y -> (Multi r) x y +> multi_R x y h = Multi_step h (Multi_refl) +> + +Third, `multi R` is _transitive_. + +> multi_trans : {t : Type} -> {r : Relation t} -> {x, y, z : t} -> +> Multi r x y -> Multi r y z -> Multi r x z +> multi_trans Multi_refl m2 = m2 +> multi_trans (Multi_step r mx) m2 = +> let indHyp = multi_trans mx m2 in +> Multi_step r indHyp +> + +In particular, for the `Multi Step` relation on terms, if `t1->>*t2` and +`t2->>*t3`, then `t1->>*t3`. + + +=== Examples + +Here's a specific instance of the `Multi Step` relation: + +> test_multistep_1 : +> P +> (P (C 0) (C 3)) +> (P (C 2) (C 4)) +> ->>* +> C ((0 + 3) + (2 + 4)) +> test_multistep_1 = +> Multi_step {y=P (C (0 + 3)) (P (C 2) (C 4))} (ST_Plus1 ST_PlusConstConst) +> (Multi_step {y=P (C (0 + 3)) (C (2 + 4))} (ST_Plus2 (V_const 3) ST_PlusConstConst) +> (Multi_step ST_PlusConstConst Multi_refl)) +> + +In fact, Idris can infer all implicits itself here: + +> test_multistep_1' : +> P +> (P (C 0) (C 3)) +> (P (C 2) (C 4)) +> ->>* +> C ((0 + 3) + (2 + 4)) +> test_multistep_1' = +> Multi_step (ST_Plus1 ST_PlusConstConst) +> (Multi_step (ST_Plus2 (V_const 3) ST_PlusConstConst) +> (Multi_step ST_PlusConstConst Multi_refl)) +> + + +==== Exercise: 1 star, optional (test_multistep_2) + +> test_multistep_2 : C 3 ->>* C 3 +> test_multistep_2 = ?test_multistep_2_rhs + +$\square$ + + +==== Exercise: 1 star, optional (test_multistep_3) + +> test_multistep_3 : +> P (C 0) (C 3) +> ->>* +> P (C 0) (C 3) +> test_multistep_3 = ?test_multistep_3_rhs +> + +$\square$ + + +==== Exercise: 2 stars (test_multistep_4) + +> test_multistep_4 : +> P +> (C 0) +> (P +> (C 2) +> (P (C 0) (C 3))) +> ->>* +> P +> (C 0) +> (C (2 + (0 + 3))) +> test_multistep_4 = ?test_multistep_4_rhs +> + +$\square$ + + +=== Normal Forms Again + +If `t` reduces to `t'` in zero or more steps and `t'` is a normal form, we say +that "`t'` is a normal form of `t`." + +> step_normal_form : (t : Tm) -> Type +> step_normal_form = normal_form Step +> +> normal_form_of : Tm -> Tm -> Type +> normal_form_of t t' = (t ->>* t', step_normal_form t') +> + +We have already seen that, for our language, single-step reduction is +deterministic -- i.e., a given term can take a single step in at most one way. +It follows from this that, if `t` can reach a normal form, then this normal form +is unique. In other words, we can actually pronounce `normal_form t t'` as +"`t'` is _the_ normal form of `t`." + + +==== Exercise: 3 stars, optional (normal_forms_unique) + +\todo[inline]{The result will likely not pass the totality checker, as it +currently has trouble looking under tuples, just use `assert_total`} + +> normal_forms_unique : deterministic Smallstep.normal_form_of +> normal_forms_unique (l,r) (l2,r2) = ?normal_forms_unique_rhs +> + +$\square$ + +Indeed, something stronger is true for this language (though not for all +languages): the reduction of _any_ term `t` will eventually reach a normal form +-- i.e., `normal_form_of` is a _total_ function. Formally, we say the `step` +relation is _normalizing_. + +> normalizing : {x : Type} -> (r : Relation x) -> Type +> normalizing {x} {r} = (t : x) -> (t' : x ** (Multi r t t', normal_form r t')) +> + +To prove that `step` is normalizing, we need a couple of lemmas. + +First, we observe that, if `t` reduces to `t'` in many steps, then the same +sequence of reduction steps within `t` is also possible when `t` appears as the +left-hand child of a `P` node, and similarly when `t` appears as the right-hand +child of a `P` node whose left-hand child is a value. + +> multistep_congr_1 : (t1 ->>* t1') -> ((P t1 t2) ->>* P t1' t2) +> multistep_congr_1 Multi_refl = Multi_refl +> multistep_congr_1 (Multi_step step mult') = +> let indHyp = multistep_congr_1 mult' in +> Multi_step (ST_Plus1 step) indHyp +> + + +==== Exercise: 2 stars (multistep_congr_2) + +> multistep_congr_2 : {v : Value t1} -> (t2 ->>* t2') -> ((P t1 t2) ->>* P t1 t2') +> multistep_congr_2 {v} mult = ?multistep_congr_2_rhs +> + +$\square$ + +With these lemmas in hand, the main proof is a straightforward induction. + +_Theorem_: The `step` function is normalizing -- i.e., for every `t` there +exists some `t'` such that `t` steps to `t'` and `t'` is a normal form. + +_Proof sketch_: By induction on terms. There are two cases to consider: + +- `t = C n` for some `n`. Here `t` doesn't take a step, and we have `t' = t`. + We can derive the left-hand side by reflexivity and the right-hand side by + observing (a) that values are normal forms (by `nf_same_as_value`) and (b) + that `t` is a value (by `v_const`). + +- `t = P t1 t2` for some `t1` and `t2`. By the IH, `t1` and `t2` have normal + forms `t1'` and `t2'`. Recall that normal forms are values (by + `nf_same_as_value`); we know that `t1' = C n1` and `t2' = C n2`, for some `n1` + and `n2`. We can combine the `->>*` derivations for `t1` and `t2` using + `multi_congr_1` and `multi_congr_2` to prove that `P t1 t2` reduces in many + steps to `C (n1 + n2)`. + +It is clear that our choice of `t' = C (n1 + n2)` is a value, which is in turn a +normal form. + +> step_normalizing : normalizing Step +> step_normalizing (C n) = (C n ** (Multi_refl, \(_**sc) => uninhabited sc)) +> step_normalizing (P l r) = +> let +> (_ ** (ih1l,ih1r)) = step_normalizing l +> (_ ** (ih2l,ih2r)) = step_normalizing r +> V_const n1 = (fst nf_same_as_value) ih1r +> V_const n2 = (fst nf_same_as_value) ih2r +> reduction : ((P l r) ->>* (C (n1 + n2))) = +> multi_trans {y=P (C n1) r} +> (multistep_congr_1 ih1l) +> (multi_trans {y=P (C n1) (C n2)} +> (multistep_congr_2 {v=V_const n1} ih2l) +> (Multi_step ST_PlusConstConst Multi_refl) +> ) +> normal_form : Not (t : Tm ** Step (C (n1 + n2)) t) = +> (snd nf_same_as_value) (V_const (n1 + n2)) +> in +> (C (n1 + n2) ** (reduction, normal_form)) +> + + +=== Equivalence of Big-Step and Small-Step + +Having defined the operational semantics of our tiny programming language in two +different ways (big-step and small-step), it makes sense to ask whether these +definitions actually define the same thing! They do, though it takes a little +work to show it. The details are left as an exercise. + +==== Exercise: 3 stars (eval__multistep) + +> eval__multistep : {t : Tm} -> {n : Nat} -> t >>> n -> t ->>* C n + +$\square$ + +The key ideas in the proof can be seen in the following picture: + +``` + P t1 t2 ->> (by ST_Plus1) + P t1' t2 ->> (by ST_Plus1) + P t1'' t2 ->> (by ST_Plus1) + ... + P (C n1) t2 ->> (by ST_Plus2) + P (C n1) t2' ->> (by ST_Plus2) + P (C n1) t2'' ->> (by ST_Plus2) + ... + P (C n1) (C n2) ->> (by ST_PlusConstConst) + C (n1 + n2) +``` + +That is, the multistep reduction of a term of the form `P t1 t2` proceeds in +three phases: + +- First, we use `ST_Plus1` some number of times to reduce `t1` to a normal form, + which must (by `nf_same_as_value`) be a term of the form `C n1` for some `n1`. + +- Next, we use `ST_Plus2` some number of times to reduce `t2` to a normal form, + which must again be a term of the form `C n2` for some `n2`. + +- Finally, we use `ST_PlusConstConst` one time to reduce `P (C n1) (C n2)` to `C + (n1 + n2)`. + +To formalize this intuition, you'll need to use the congruence lemmas from above +(you might want to review them now, so that you'll be able to recognize when +they are useful), plus some basic properties of `->>*`: that it is reflexive, +transitive, and includes `->>`. + +> eval__multistep hyp = ?eval__multistep_rhs + + +==== Exercise: 3 stars, advanced (eval__multistep_inf) + +Write a detailed informal version of the proof of `eval__multistep` + +$\square$ + +For the other direction, we need one lemma, which establishes a relation between +single-step reduction and big-step evaluation. + + +==== Exercise: 3 stars (step__eval) + +> step__eval : {t, t' : Tm} -> {n : Nat} -> +> t >>- t' -> +> t' >>> n -> +> t >>> n +> step__eval step eval = ?step__eval_rhs +> + +$\square$ + +The fact that small-step reduction implies big-step evaluation is now +straightforward to prove, once it is stated correctly. + +The proof proceeds by induction on the multi-step reduction sequence that is +buried in the hypothesis `normal_form_of t t'`. + +Make sure you understand the statement before you start to work on the proof. + + +==== Exercise: 3 stars (multistep__eval) + +\todo[inline]{The proof will likely not pass the totality checker, use +`assert_total`} + +> multistep__eval : {t, t' : Tm} -> +> normal_form_of t t' -> (n : Nat ** (t' = C n, t >>> n)) +> multistep__eval hyp = ?multistep__eval_rhs +> + +$\square$ + + +=== Additional Exercises + + +==== Exercise: 3 stars, optional (interp_tm) + +Remember that we also defined big-step evaluation of terms as a function +`evalF`. Prove that it is equivalent to the existing semantics. (Hint: we just +proved that `Eval` and `Multi Step` are equivalent, so logically it doesn't +matter which you choose. One will be easier than the other, though!) + +> evalF_eval : {t : Tm} -> {n : Nat} -> ((evalF t = n) <-> (t >>> n)) +> evalF_eval = ?evalF_eval_rhs +> + +$\square$ + + +==== Exercise: 4 stars (combined_properties) + +We've considered arithmetic and conditional expressions separately. This +exercise explores how the two interact. + +> data TmC : Type where +> CC : Nat -> TmC +> PC : TmC -> TmC -> TmC +> TtrueC : TmC +> TfalseC : TmC +> TifC : TmC -> TmC -> TmC -> TmC +> +> data ValueC : TmC -> Type where +> V_constC : {n : Nat} -> ValueC (CC n) +> V_trueC : ValueC TtrueC +> V_falseC : ValueC TfalseC +> +> mutual +> infixl 6 >>-> +> (>>->) : TmC -> TmC -> Type +> (>>->) = StepC +> +> data StepC : TmC -> TmC -> Type where +> ST_PlusConstConstC : PC (CC n1) (CC n2) >>-> CC (n1 + n2) +> ST_Plus1C : t1 >>-> t1' -> PC t1 t2 >>-> PC t1' t2 +> ST_Plus2C : ValueC v1 -> t2 >>-> t2' -> PC v1 t2 >>-> PC v1 t2' +> ST_IfTrueC : TifC TtrueC t1 t2 >>-> t1 +> ST_IfFalseC : TifC TfalseC t1 t2 >>-> t2 +> ST_IfC : t1 >>-> t1' -> TifC t1 t2 t3 >>-> TifC t1' t2 t3 +> + +Earlier, we separately proved for both plus- and if-expressions... + +- that the step relation was deterministic, and + +- a strong progress lemma, stating that every term is either a value or can take +a step. + +Formally prove or disprove these two properties for the combined language. (That +is, state a theorem saying that the property holds or does not hold, and prove +your theorem.) + +$\square$ + + +== Small-Step Imp + +Now for a more serious example: a small-step version of the Imp operational +semantics. + +The small-step reduction relations for arithmetic and boolean expressions are +straightforward extensions of the tiny language we've been working up to now. To +make them easier to read, we introduce the symbolic notations `->>a` and `->>b` +for the arithmetic and boolean step relations. + +> data AVal : AExp -> Type where +> Av_num : AVal (ANum n) +> + +We are not actually going to bother to define boolean values, since they aren't +needed in the definition of `->>b` below (why?), though they might be if our +language were a bit larger (why?). + +> data AStep : AExp -> State -> AExp -> Type where +> AS_Id : AStep (AId i) +> st (ANum (st i)) +> AS_Plus : AStep (APlus (ANum n1) (ANum n2)) +> st (ANum (n1 + n2)) +> AS_Plus1 : AStep a1 st a1' -> AStep (APlus a1 a2) +> st (APlus a1' a2) +> AS_Plus2 : AVal v1 -> AStep a2 st a2' -> AStep (APlus v1 a2) +> st (APlus v1 a2') +> AS_Minus : AStep (AMinus (ANum n1) (ANum n2)) +> st (ANum (minus n1 n2)) +> AS_Minus1 : AStep a1 st a1' -> AStep (AMinus a1 a2) +> st (AMinus a1' a2) +> AS_Minus2 : AVal v1 -> AStep a2 st a2' -> AStep (AMinus v1 a2) +> st (AMinus v1 a2') +> AS_Mult : AStep (AMult (ANum n1) (ANum n2)) +> st (ANum (mult n1 n2)) +> AS_Mult1 : AStep a1 st a1' -> AStep (AMult a1 a2) +> st (AMult a1' a2) +> AS_Mult2 : AVal v1 -> AStep a2 st a2' -> AStep (AMult v1 a2) +> st (AMult v1 a2') +> +> data BStep : BExp -> State -> BExp -> Type where +> BS_Eq : BStep (BEq (ANum n1) (ANum n2)) +> st (if (n1==n2) then BTrue else BFalse) +> BS_Eq1 : AStep a1 st a1' -> BStep (BEq a1 a2) +> st (BEq a1' a2) +> BS_Eq2 : AVal v1 -> AStep a2 st a2' -> BStep (BEq v1 a2) +> st (BEq v1 a2') +> BS_LtEq : BStep (BLe (ANum n1) (ANum n2)) +> st (if (n1<=n2) then BTrue else BFalse) +> BS_LtEq1 : AStep a1 st a1' -> BStep (BLe a1 a2) +> st (BLe a1' a2) +> BS_LtEq2 : AVal v1 -> AStep a2 st a2' -> BStep (BLe v1 a2) +> st (BLe v1 a2') +> BS_NotTrue : BStep (BNot BTrue) +> st BFalse +> BS_NotFalse : BStep (BNot BFalse) +> st BTrue +> BS_NotStep : BStep b1 st b1' -> BStep (BNot b1) +> st (BNot b1') +> BS_AndTrueTrue : BStep (BAnd BTrue BTrue) +> st BTrue +> BS_AndTrueFalse : BStep (BAnd BTrue BFalse) +> st BFalse +> BS_AndFalse : BStep (BAnd BFalse b2) +> st BFalse +> BS_AndTrueStep : BStep b2 st b2' -> BStep (BAnd BTrue b2) +> st (BAnd BTrue b2') +> BS_AndStep : BStep b1 st b1' -> BStep (BAnd b1 b2) +> st (BAnd b1' b2) +> + +The semantics of commands is the interesting part. We need two small tricks to +make it work: + +- We use `SKIP` as a "command value" -- i.e., a command that has reached a + normal form. + + - An assignment command reduces to `SKIP` (and an updated state). + + - The sequencing command waits until its left-hand subcommand has reduced to + `SKIP`, then throws it away so that reduction can continue with the + right-hand subcommand. + +- We reduce a `WHILE` command by transforming it into a conditional followed by + the same `WHILE`. + +(There are other ways of achieving the effect of the latter trick, but they all +share the feature that the original `WHILE` command needs to be saved somewhere +while a single copy of the loop body is being reduced.) + +> data CStep : (Com, State) -> (Com, State) -> Type where +> CS_AssStep : AStep a st a' -> CStep (CAss i a , st) +> (CAss i a', st) +> CS_Ass : CStep (CAss i (ANum n), st ) +> (CSkip , t_update i n st) +> CS_SeqStep : CStep (c1, st) (c1', st') -> CStep (CSeq c1 c2, st ) +> (CSeq c1' c2, st') +> CS_SeqFinish : CStep (CSeq CSkip c2, st) +> (c2 , st) +> CS_IfTrue : CStep (CIf BTrue c1 c2, st) +> (c1 , st) +> CS_IfFalse : CStep (CIf BFalse c1 c2, st) +> (c2 , st) +> CS_IfStep : BStep b st b' -> CStep (CIf b c1 c2, st) +> (CIf b' c1 c2, st) +> CS_While : CStep (CWhile b c1 , st) +> (CIf b (CSeq c1 (CWhile b c1)) CSkip, st) +> + + +== Concurrent Imp + +Finally, to show the power of this definitional style, let's enrich Imp with a +new form of command that runs two subcommands in parallel and terminates when +both have terminated. To reflect the unpredictability of scheduling, the +actions of the subcommands may be interleaved in any order, but they share the +same memory and can communicate by reading and writing the same variables. + +> data ComC : Type where +> CSkipC : ComC +> CAssC : Id -> AExp -> ComC +> CSeqC : ComC -> ComC -> ComC +> CIfC : BExp -> ComC -> ComC -> ComC +> CWhileC : BExp -> ComC -> ComC +> -- New: +> CParC : ComC -> ComC -> ComC +> + +\todo[inline]{Add syntax sugar} + +> data CStepC : (ComC, State) -> (ComC, State) -> Type where +> -- Old part +> CS_AssStepC : AStep a st a' -> CStepC (CAssC i a , st) +> (CAssC i a', st) +> CS_AssC : CStepC (CAssC i (ANum n), st) +> (CSkipC , t_update i n st) +> CS_SeqStepC : CStepC (c1, st) (c1', st') -> CStepC (CSeqC c1 c2, st ) +> (CSeqC c1' c2, st') +> CS_SeqFinishC : CStepC (CSeqC CSkipC c2, st) +> (c2 , st) +> CS_IfTrueC : CStepC (CIfC BTrue c1 c2, st) +> (c1 , st) +> CS_IfFalseC : CStepC (CIfC BFalse c1 c2, st) +> (c2 , st) +> CS_IfStepC : BStep b st b' -> CStepC (CIfC b c1 c2, st) +> (CIfC b' c1 c2, st) +> CS_WhileC : CStepC (CWhileC b c1 , st) +> (CIfC b (CSeqC c1 (CWhileC b c1)) CSkipC, st) +> -- New part: +> CS_Par1 : CStepC (c1, st) (c1', st') -> CStepC (CParC c1 c2, st ) +> (CParC c1' c2, st') +> CS_Par2 : CStepC (c2, st) (c2', st') -> CStepC (CParC c1 c2 , st ) +> (CParC c1 c2', st') +> CS_ParDone : CStepC (CParC CSkipC CSkipC, st) +> (CSkipC , st) +> +> MultiCStepC : (ComC, State) -> (ComC, State) -> Type +> MultiCStepC = Multi CStepC +> + +Among the many interesting properties of this language is the fact that the +following program can terminate with the variable `X` set to any value + +> par_loop : ComC +> par_loop = CParC +> (CAssC Y (ANum 1)) +> (CWhileC +> (BEq (AId Y) (ANum 0)) +> (CAssC X (APlus (AId X) (ANum 1))) +> ) +> + +In particular, it can terminate with `X` set to `0`: + +> par_loop_example_0 : (st' ** ( MultiCStepC (Smallstep.par_loop, Imp.empty_state) +> (CSkipC, st') +> , st' X = 0 +> )) +> par_loop_example_0 = +> (t_update Y 1 (t_empty 0) ** +> ( +> Multi_step (CS_Par1 CS_AssC) $ +> Multi_step (CS_Par2 CS_WhileC) $ +> Multi_step (CS_Par2 $ CS_IfStepC $ BS_Eq1 AS_Id) $ +> Multi_step (CS_Par2 $ CS_IfStepC $ BS_Eq) $ +> Multi_step (CS_Par2 $ CS_IfFalseC) $ +> Multi_step CS_ParDone $ +> Multi_refl +> +> , Refl +> ) +> ) +> + +It can also terminate with `X` set to `2`: + +> par_loop_example_2 : (st' ** ( MultiCStepC (Smallstep.par_loop, Imp.empty_state) +> (CSkipC, st') +> , st' X = 2 +> )) +> par_loop_example_2 = +> (t_update Y 1 (t_update X 2 (t_update X 1 (t_empty 0))) ** +> ( +> Multi_step (CS_Par2 CS_WhileC) $ +> Multi_step (CS_Par2 $ CS_IfStepC $ BS_Eq1 AS_Id) $ +> Multi_step (CS_Par2 $ CS_IfStepC $ BS_Eq) $ +> Multi_step (CS_Par2 $ CS_IfTrueC) $ +> Multi_step (CS_Par2 $ CS_SeqStepC $ CS_AssStepC $ AS_Plus1 AS_Id) $ +> Multi_step (CS_Par2 $ CS_SeqStepC $ CS_AssStepC AS_Plus) $ +> Multi_step (CS_Par2 $ CS_SeqStepC $ CS_AssC) $ +> Multi_step (CS_Par2 CS_SeqFinishC) $ +> +> Multi_step (CS_Par2 CS_WhileC) $ +> Multi_step (CS_Par2 $ CS_IfStepC $ BS_Eq1 AS_Id) $ +> Multi_step (CS_Par2 $ CS_IfStepC $ BS_Eq) $ +> Multi_step (CS_Par2 $ CS_IfTrueC) $ +> Multi_step (CS_Par2 $ CS_SeqStepC $ CS_AssStepC $ AS_Plus1 AS_Id) $ +> Multi_step (CS_Par2 $ CS_SeqStepC $ CS_AssStepC AS_Plus) $ +> Multi_step (CS_Par2 $ CS_SeqStepC $ CS_AssC) $ +> Multi_step (CS_Par2 CS_SeqFinishC) $ +> +> Multi_step (CS_Par1 CS_AssC) $ +> Multi_step (CS_Par2 CS_WhileC) $ +> Multi_step (CS_Par2 $ CS_IfStepC $ BS_Eq1 AS_Id) $ +> Multi_step (CS_Par2 $ CS_IfStepC $ BS_Eq) $ +> Multi_step (CS_Par2 $ CS_IfFalseC) $ +> Multi_step CS_ParDone $ +> Multi_refl +> +> , Refl +> ) +> ) +> + +More generally... + + +==== Exercise: 3 stars, optional (par_body_n__Sn) + +> par_body_n_Sn : (n : Nat) -> st X = n -> st Y = 0 -> MultiCStepC (Smallstep.par_loop, st) +> (Smallstep.par_loop, t_update X (S n) st) +> par_body_n_Sn n stx sty = ?par_body_n_Sn_rhs +> + +$\square$ + + +==== Exercise: 3 stars, optional (par_body_n) + +> par_body_n : (n : Nat) -> st X = 0 -> st Y = 0 -> (st' ** ( MultiCStepC (Smallstep.par_loop, st) +> (Smallstep.par_loop, st') +> , st' X = n +> , st' Y = 0 +> )) +> par_body_n n {st} stx sty = ?par_body_n_rhs +> + +$\square$ + +... the above loop can exit with `X` having any value whatsoever. + +> par_loop_any_X : (n : Nat) -> (st' ** ( MultiCStepC (Smallstep.par_loop, Imp.empty_state) +> (CSkipC, st') +> , st' X = n +> )) +> par_loop_any_X n = +> let (st1 ** (ms, stx, sty)) = par_body_n n {st=Imp.empty_state} Refl Refl in +> (t_update Y 1 st1 ** ( multi_trans ms $ +> Multi_step (CS_Par1 CS_AssC) $ +> Multi_step (CS_Par2 CS_WhileC) $ +> Multi_step (CS_Par2 $ CS_IfStepC $ BS_Eq1 AS_Id) $ +> Multi_step (CS_Par2 $ CS_IfStepC $ BS_Eq) $ +> Multi_step (CS_Par2 $ CS_IfFalseC) $ +> Multi_step CS_ParDone $ +> Multi_refl +> , stx +> )) +> + + +== A Small-Step Stack Machine + +Our last example is a small-step semantics for the stack machine example from +the `Imp` chapter of _Logical Foundations_. + +> Stack : Type +> Stack = List Nat +> +> Prog : Type +> Prog = List SInstr +> +> data StackStep : State -> (Prog, Stack) -> (Prog, Stack) -> Type where +> SS_Push : StackStep st (SPush n :: p, stk) (p, n :: stk) +> SS_Load : StackStep st (SLoad i :: p, stk ) (p, st i :: stk) +> SS_Plus : StackStep st (SPlus :: p, n::m::stk) (p, m + n :: stk) +> SS_Minus : StackStep st (SMinus :: p, n::m::stk) (p, (m `minus` n):: stk) +> SS_Mult : StackStep st (SMult :: p, n::m::stk) (p, m * n :: stk) +> +> stack_step_deterministic : deterministic (StackStep st) +> stack_step_deterministic SS_Push SS_Push = Refl +> stack_step_deterministic SS_Load SS_Load = Refl +> stack_step_deterministic SS_Plus SS_Plus = Refl +> stack_step_deterministic SS_Minus SS_Minus = Refl +> stack_step_deterministic SS_Mult SS_Mult = Refl +> +> StackMultistep : State -> (Prog, Stack) -> (Prog, Stack) -> Type +> StackMultistep st = Multi (StackStep st) +> + + +==== Exercise: 3 stars, advanced (compiler_is_correct) + +Remember the definition of `compile` for `AExp` given in the `Imp` chapter of +_Logical Foundations_. We want now to prove `compile` correct with respect to +the stack machine. + +State what it means for the compiler to be correct according to the stack +machine small step semantics and then prove it. + +> Compiler_is_correct_statement : Type +> Compiler_is_correct_statement = ?compiler_is_correct_statement_rhs +> +> compiler_is_correct : Compiler_is_correct_statement +> compiler_is_correct = ?compiler_is_correct_rhs +> + +$\square$ diff --git a/src/Stlc.lidr b/src/Stlc.lidr new file mode 100644 index 0000000..a82fea8 --- /dev/null +++ b/src/Stlc.lidr @@ -0,0 +1,777 @@ += Stlc + +== Stlc : The Simply Typed Lambda-Calculus + +The simply typed lambda-calculus (STLC) is a tiny core +calculus embodying the key concept of _functional abstraction_, +which shows up in pretty much every real-world programming +language in some form (functions, procedures, methods, etc.). + +We will follow exactly the same pattern as in the previous chapter +when formalizing this calculus (syntax, small-step semantics, +typing rules) and its main properties (progress and preservation). +The new technical challenges arise from the mechanisms of +_variable binding_ and _substitution_. It which will take some +work to deal with these. + +> module Stlc +> import Smallstep +> import Types +> import Maps + +> %access public export +> %default total + +> %hide Types.Tm +> %hide Types.Ty +> %hide Types.(->>) +> %hide Types.(->>*) +> %hide Smallstep.(->>) +> %hide Smallstep.(->>*) +> %hide Types.Has_type + +=== Overview + +The STLC is built on some collection of _base types_: +booleans, numbers, strings, etc. The exact choice of base types +doesn't matter much -- the construction of the language and its +theoretical properties work out the same no matter what we +choose -- so for the sake of brevity let's take just `Bool` for +the moment. At the end of the chapter we'll see how to add more +base types, and in later chapters we'll enrich the pure STLC with +other useful constructs like pairs, records, subtyping, and +mutable state. + +Starting from boolean constants and conditionals, we add three +things: + - variables + - function abstractions + - application + +This gives us the following collection of abstract syntax +constructors (written out first in informal BNF notation -- we'll +formalize it below). + +``` + t ::= x variable + | \x:T1.t2 abstraction + | t1 t2 application + | true constant true + | false constant false + | if t1 then t2 else t3 conditional +``` + +The `\` symbol in a function abstraction `\x:T1.t2` is generally +written as a Greek letter "lambda" (hence the name of the +calculus). The variable `x` is called the _parameter_ to the +function; the term `t2` is its _body_. The annotation `:T1` +specifies the type of arguments that the function can be applied +to. + +Some examples: + +- `\x:Bool. x` + + The identity function for booleans. + +- `(\x:Bool. x) true` + + The identity function for booleans, applied to the boolean `true`. + +- `\x:Bool. if x then false else true` + + The boolean "not" function. + +- `\x:Bool. true` + + The constant function that takes every (boolean) argument to + `true`. + +- `\x:Bool. \y:Bool. x` + + A two-argument function that takes two booleans and returns + the first one. (As in Coq, a two-argument function is really + a one-argument function whose body is also a one-argument + function.) + +- `(\x:Bool. \y:Bool. x) false true` + + A two-argument function that takes two booleans and returns + the first one, applied to the booleans `false` and `true`. + + As in Coq, application associates to the left -- i.e., this + expression is parsed as `((\x:Bool. \y:Bool. x) false) true`. + +- `\f:Bool->Bool. f (f true)` + + A higher-order function that takes a _function_ `f` (from + booleans to booleans) as an argument, applies `f` to `true`, + and applies `f` again to the result. + +- `(\f:Bool->Bool. f (f true)) (\x:Bool. false)` + + The same higher-order function, applied to the constantly + `false` function. + +As the last several examples show, the STLC is a language of +_higher-order_ functions: we can write down functions that take +other functions as arguments and/or return other functions as +results. + +The STLC doesn't provide any primitive syntax for defining _named_ +functions -- all functions are "anonymous." We'll see in chapter +`MoreStlc` that it is easy to add named functions to what we've +got -- indeed, the fundamental naming and binding mechanisms are +exactly the same. + +The _types_ of the STLC include `Bool`, which classifies the +boolean constants `true` and `false` as well as more complex +computations that yield booleans, plus _arrow types_ that classify +functions. + +``` + T ::= Bool + | T1 -> T2 +``` + +For example: + + - `\x:Bool. false` has type `Bool->Bool` + + - `\x:Bool. x` has type `Bool->Bool` + + - `(\x:Bool. x) true` has type `Bool` + + - `\x:Bool. \y:Bool. x` has type `Bool->Bool->Bool` + (i.e., `Bool -> (Bool->Bool)`) + + - `(\x:Bool. \y:Bool. x) false` has type `Bool->Bool` + + - `(\x:Bool. \y:Bool. x) false true` has type `Bool` *) + + +=== Syntax + +We next formalize the syntax of the STLC. + +==== Types + +> data Ty : Type where +> TBool : Ty +> TArrow : Ty -> Ty -> Ty + +> infixr 0 :=> +> (:=>) : Ty -> Ty -> Ty +> (:=>) = TArrow + + +==== Terms + +> infixr 7 # + +> data Tm : Type where +> Tvar : Id -> Tm +> (#) : Tm -> Tm -> Tm +> Tabs : Id -> Ty -> Tm -> Tm +> Ttrue : Tm +> Tfalse : Tm +> Tif : Tm -> Tm -> Tm -> Tm + +> syntax "(" "\\" [p] ":" [q] "." [r] ")" = Tabs (MkId "p") q r + +> syntax "lif" [c] "then" [p] "else" [n] = Tif c p n + +> var : String -> Tm +> var s = Tvar (MkId s) + +Note that an abstraction `\x:T.t` (formally, `tabs x T t`) is +always annotated with the type `T` of its :parameter, in contrast +to Idris (and other functional languages like ML, Haskell, etc.), +which use type inference to fill in missing annotations. We're +not considering type inference here. + +Some examples... + +`idB = \x:Bool. x` + +> idB : Tm +> idB = (\x: TBool . var "x") + +`idBB = \x:Bool->Bool. x` + +> idBB : Tm +> idBB = (\x: (TBool :=> TBool) . var "x") + +`idBBBB = \x:(Bool->Bool) -> (Bool->Bool). x` + +> idBBBB : Tm +> idBBBB = (\x: ((TBool :=> TBool) :=> (TBool :=> TBool)). var "x") + +`k = \x:Bool. \y:Bool. x` + +> k : Tm +> k = (\x : TBool . (\y : TBool . var "x")) + +`notB = \x:Bool. if x then false else true` + +> notB : Tm +> notB = (\x : TBool . (lif (var "x") then Tfalse else Ttrue)) + +=== Operational Semantics + +To define the small-step semantics of STLC terms, we begin, +as always, by defining the set of values. Next, we define the +critical notions of _free variables_ and _substitution_, which are +used in the reduction rule for application expressions. And +finally we give the small-step relation itself. + +==== Values + +To define the values of the STLC, we have a few cases to consider. + +First, for the boolean part of the language, the situation is +clear: `true` and `false` are the only values. An `if` +expression is never a value. + +Second, an application is clearly not a value: It represents a +function being invoked on some argument, which clearly still has +work left to do. + +Third, for abstractions, we have a choice: + + - We can say that `\x:T. t1` is a value only when `t1` is a + value -- i.e., only if the function's body has been + reduced (as much as it can be without knowing what argument it + is going to be applied to). + + - Or we can say that `\x:T. t1` is always a value, no matter + whether `t1` is one or not -- in other words, we can say that + reduction stops at abstractions. + +Our usual way of evaluating expressions in Idris makes the first +choice -- for example, + + Compute (fun x:bool => 3 + 4) + + yields `fun x:bool => 7`. + +Most real-world functional programming languages make the second +choice -- reduction of a function's body only begins when the +function is actually applied to an argument. We also make the +second choice here. + +> data Value : Tm -> Type where +> V_abs : {x: Id} -> {T: Ty} -> {t: Tm} -> Value (Tabs x T t) +> V_true : Value Ttrue +> V_false : Value Tfalse + +Finally, we must consider what constitutes a _complete_ program. + +Intuitively, a "complete program" must not refer to any undefined +variables. We'll see shortly how to define the _free_ variables +in a STLC term. A complete program is _closed_ -- that is, it +contains no free variables. + +(Conversely, a term with free variables is often called an _open +term_.) + +Having made the choice not to reduce under abstractions, we don't +need to worry about whether variables are values, since we'll +always be reducing programs "from the outside in," and that means +the `step` relation will always be working with closed terms. + +==== Substitution + +Now we come to the heart of the STLC: the operation of +substituting one term for a variable in another term. This +operation is used below to define the operational semantics of +function application, where we will need to substitute the +argument term for the function parameter in the function's body. +For example, we reduce + + (\x:Bool. if x then true else x) false + +to + + if false then true else false + +by substituting `false` for the parameter `x` in the body of the +function. + +In general, we need to be able to substitute some given term `s` +for occurrences of some variable `x` in another term `t`. In +informal discussions, this is usually written ` [x:=s]t ` and +pronounced "substitute `x` with `s` in `t`." + +Here are some examples: + + - `[x:=true] (if x then x else false)` + yields `if true then true else false` + + - `[x:=true] x` yields `true` + + - `[x:=true] (if x then x else y)` yields `if true then true else y` + + - `[x:=true] y` yields `y` + + - `[x:=true] false` yields `false` (vacuous substitution) + + - `[x:=true] (\y:Bool. if y then x else false)` + yields `\y:Bool. if y then true else false` + + - `[x:=true] (\y:Bool. x)` yields `\y:Bool. true` + + - `[x:=true] (\y:Bool. y)` yields `\y:Bool. y` + + - `[x:=true] (\x:Bool. x)` yields `\x:Bool. x` + +The last example is very important: substituting `x` with `true` in +`\x:Bool. x` does _not_ yield `\x:Bool. true`! The reason for +this is that the `x` in the body of `\x:Bool. x` is _bound_ by the +abstraction: it is a new, local name that just happens to be +spelled the same as some global name `x`. + +Here is the definition, informally... + + + [x:=s]x = s + [x:=s]y = y if x <> y + [x:=s](\x:T11. t12) = \x:T11. t12 + [x:=s](\y:T11. t12) = \y:T11. [x:=s]t12 if x <> y + [x:=s](t1 t2) = ([x:=s]t1) ([x:=s]t2) + [x:=s]true = true + [x:=s]false = false + [x:=s](if t1 then t2 else t3) = + if [x:=s]t1 then [x:=s]t2 else [x:=s]t3 + +... and formally: + +> subst : Id -> Tm -> Tm -> Tm +> subst x s (Tvar x') = +> case decEq x x' of +> Yes => s +> No _ => Tvar x' +> subst x s (Tabs x' ty t1) = +> case decEq x x' of +> Yes => t1 +> No _ => subst x s t1 +> subst x s (t1 # t2) = subst x s t1 # subst x s t2 +> subst x s Ttrue = Ttrue +> subst x s Tfalse = Tfalse +> subst x s (Tif t1 t2 t3) = Tif (subst x s t1) (subst x s t2) (subst x s t3) + +> syntax "[" [p] ":=" [q] "]" [r] = subst p q r + +_Technical note_: Substitution becomes trickier to define if we +consider the case where `s`, the term being substituted for a +variable in some other term, may itself contain free variables. +Since we are only interested here in defining the `step` relation +on _closed_ terms (i.e., terms like `\x:Bool. x` that include +binders for all of the variables they mention), we can avoid this +extra complexity here, but it must be dealt with when formalizing +richer languages. + +For example, using the definition of substitution above to +substitute the _open_ term `s = \x:Bool. r`, where `r` is a _free_ +reference to some global resource, for the variable `z` in the +term `t = \r:Bool. z`, where `r` is a bound variable, we would get +`\r:Bool. \x:Bool. r`, where the free reference to `r` in `s` has +been "captured" by the binder at the beginning of `t`. + +Why would this be bad? Because it violates the principle that the +names of bound variables do not matter. For example, if we rename +the bound variable in `t`, e.g., let `t' = \w:Bool. z`, then +`[x:=s]t` is `\w:Bool. \x:Bool. r`, which does not behave the +same as `[x:=s]t = \r:Bool. \x:Bool. r`. That is, renaming a +bound variable changes how `t` behaves under substitution. + +See, for example, `Aydemir 2008` for further discussion +of this issue. + +==== Exercise: 3 stars (substi_correct) + +The definition that we gave above uses Idris recursive facility +to define substitution as a _function_. Suppose, instead, we +wanted to define substitution as an inductive _relation_ `substi`. +We've begun the definition by providing the `Inductive` header and +one of the constructors; your job is to fill in the rest of the +constructors and prove that the relation you've defined coincides +with the function given above. + +> data Substi : (s:Tm) -> (x:Id) -> Tm -> Tm -> Type where +> S_True : Substi s x Ttrue Ttrue +> S_False : Substi s x Tfalse Tfalse +> S_App : {l', r':Tm} -> Substi s x l l' -> Substi s x r r' -> Substi s x (l # r) (l' # r') +> S_If : {b', p',n':Tm} -> Substi s x b b' -> Substi s x p p' +> -> Substi s x n n' -> Substi s x (Tif b p n) (Tif b' p' n') +> S_Var1 : Substi s x (Tvar x) s +> S_Var2 : Substi s x (Tvar y) (Tvar y) +> S_Abs1 : Substi s x t t' -> Substi s x (Tabs x' ty t) (Tabs x' ty t') +> S_Abs2 : Substi s x (Tabs y ty t) (Tabs y ty t) + + +> substi_correct : (s:Tm) -> (x: Id) -> (t : Tm) -> (t' : Tm) -> +> (([ x := s ] t) = t') <-> Substi s x t t' +> substi_correct s x t t' = ?substi_correct_rhs1 + +$\square$ + +== Reduction + +The small-step reduction relation for STLC now follows the +same pattern as the ones we have seen before. Intuitively, to +reduce a function application, we first reduce its left-hand +side (the function) until it becomes an abstraction; then we +reduce its right-hand side (the argument) until it is also a +value; and finally we substitute the argument for the bound +variable in the body of the abstraction. This last rule, written +informally as + + (\x:T.t12) v2 ->> [x:=v2] t12 + +is traditionally called "beta-reduction". + + +\[ + \begin{prooftree} + \hypo{\idr{value v2}} + \infer1[\idr{ST_AppAbs}]{\idr{(\x:T.t12) v2 ->> [x:=v2] t12}} + \end{prooftree} +\] + +\[ + \begin{prooftree} + \hypo{\idr{t1 ->> t1'}} + \infer1[\idr{ST_App1}]{\idr{t1 t2 ->> t1' t2}} + \end{prooftree} +\] + +\[ + \begin{prooftree} + \hypo{\idr{value v1}} + \hypo{\idr{t2 ->> t2'}} + \infer2[\idr{ST_App2}]{\idr{v1 t2 ->> v1 t2'}} + \end{prooftree} +\] + +... plus the usual rules for conditionals: + +\[ + \begin{prooftree} + \infer0[\idr{ST_IfTrue}]{\idr{(if true then t1 else t2) ->> t1}} + \end{prooftree} +\] + +\[ + \begin{prooftree} + \infer0[\idr{ST_IfFalse}]{\idr{(if false then t1 else t2) ->> t2}} + \end{prooftree} +\] + +\[ + \begin{prooftree} + \hypo{\idr{t1 ->> t1'}} + \infer1[\idr{ST_If}]{\idr{(if t1 then t2 else t3) ->> (if t1' then t2 else t3)}} + \end{prooftree} +\] + +Formally: + +> mutual +> infixl 6 ->> +> (->>) : Tm -> Tm -> Type +> (->>) = Step +> +> data Step : Tm -> Tm -> Type where +> ST_AppAbs : {x: Id} -> {ty : Ty} -> {t12 : Tm} -> {v2 : Tm} -> +> Value v2 -> +> (Tabs x ty t12) # v2 ->> subst x v2 t12 +> ST_App1 : {t1, t1', t2: Tm} -> +> t1 ->> t1' -> +> t1 # t2 ->> t1' # t2 +> ST_App2 : {v1, t2, t2' : Tm} -> +> Value v1 -> +> t2 ->> t2' -> +> v1 # t2 ->> v1 # t2' +> ST_IfTrue : {t1, t2: Tm} -> +> Tif Ttrue t1 t2 ->> t1 +> ST_IfFalse : {t1, t2: Tm} -> +> Tif Tfalse t1 t2 ->> t2 +> ST_If : {t1, t1', t2, t3: Tm} -> +> t1 ->> t1' -> +> Tif t1 t2 t3 ->> Tif t1' t2 t3 + +> infixl 6 ->>* +> (->>*) : Tm -> Tm -> Type +> (->>*) t t' = Multi Step t t' + +=== Examples + +Example: + + (\x:Bool->Bool. x) (\x:Bool. x) ->>* \x:Bool. x + + i.e., + + idBB idB ->>* idB + +> step_example1 : Stlc.idBB # Stlc.idB ->>* Stlc.idB +> step_example1 = Multi_step (ST_AppAbs V_abs) Multi_refl + +Example: + + (\x:Bool->Bool. x) ((\x:Bool->Bool. x) (\x:Bool. x)) + ->>* \x:Bool. x + + i.e., + + (idBB (idBB idB)) ->>* idB. + +> step_example2 : Stlc.idBB # (Stlc.idBB # Stlc.idB) ->>* Stlc.idB +> step_example2 = +> Multi_step (ST_App2 V_abs (ST_AppAbs V_abs)) +> (Multi_step (ST_AppAbs V_abs) Multi_refl) + +Example: + + (\x:Bool->Bool. x) + (\x:Bool. if x then false else true) + true + ->>* false + + i.e., + + (idBB notB) ttrue ->>* tfalse. + +> step_example3 : (Stlc.idBB # Stlc.notB) # Ttrue ->>* Tfalse +> step_example3 = Multi_step (ST_App1 (ST_AppAbs V_abs)) +> (Multi_step (ST_AppAbs V_true) +> (Multi_step ST_IfTrue Multi_refl)) + +Example: + + (\x:Bool -> Bool. x) + ((\x:Bool. if x then false else true) true) + ->>* false + + i.e., + + idBB (notB ttrue) ->>* tfalse. + +(Note that this term doesn't actually typecheck; even so, we can +ask how it reduces.) + +> step_example4 : Stlc.idBB # (Stlc.notB # Ttrue) ->>* Tfalse +> step_example4 = Multi_step (ST_App2 V_abs (ST_AppAbs V_true)) +> (Multi_step (ST_App2 V_abs ST_IfTrue) +> (Multi_step (ST_AppAbs V_false) Multi_refl)) + + + +==== Exercise: 2 stars (step_example5) + +> step_example5 : +> (Stlc.idBBBB # Stlc.idBB) # Stlc.idB ->>* Stlc.idB +> step_example5 = ?step_example5_rhs + +$\square$ + +=== Typing + +Next we consider the typing relation of the STLC. + +==== Contexts + +_Question_: What is the type of the term "`x y`" + +_Answer_: It depends on the types of `x` and `y`! + +I.e., in order to assign a type to a term, we need to know +what assumptions we should make about the types of its free +variables. + +This leads us to a three-place _typing judgment_, informally +written `Gamma |- t ::T`, where `Gamma` is a +"typing context" -- a mapping from variables to their types. + +Following the usual notation for partial maps, we could write `Gamma +& {{x:T}}` for "update the partial function `Gamma` to also map +`x` to `T`." + +> Context : Type +> Context = PartialMap Ty + +> syntax [context] "&" "{{" [x] "==>" [y] "}}" = update x y context + +==== Typing Relation + +\[ + \begin{prooftree} + \hypo{\idr{Gamma x = T}} + \infer1[\idr{T_Var}]{\idr{Gamma |- x ::T}} + \end{prooftree} +\] + +\[ + \begin{prooftree} + \hypo{\idr{Gamma & {{ x ==> T11 }} |- t12 :: T12}} + \infer1[\idr{T_Abs}]{\idr{Gamma |- \x:T11.t12 ::T11->T12}} + \end{prooftree} +\] + +\[ + \begin{prooftree} + \hypo{\idr{Gamma |- t1 ::T11->T12}} + \hypo{\idr{Gamma |- t2 ::T11}} + \infer2[\idr{T_App}]{\idr{Gamma |- t1 t2 ::T12}} + \end{prooftree} +\] + +\[ + \begin{prooftree} + \infer0[\idr{T_True}]{\idr{Gamma |- true ::Bool}} + \end{prooftree} +\] + +\[ + \begin{prooftree} + \infer0[\idr{T_False}]{\idr{Gamma |- false ::Bool}} + \end{prooftree} +\] + +\[ + \begin{prooftree} + \hypo{\idr{Gamma |- t1 ::Bool}} + \hypo{\idr{Gamma |- t2 ::T}} + \hypo{\idr{Gamma |- t3 ::T}} + \infer3[\idr{T_If}]{\idr{Gamma |- if t1 then t2 else t3 ::T}} + \end{prooftree} +\] + +We can read the three-place relation `Gamma |- t ::T` as: +"under the assumptions in Gamma, the term `t` has the type `T`." *) + +> syntax [context] "|-" [t] "::" [T] = Has_type context t T + +> data Has_type : Context -> Tm -> Ty -> Type where +> T_Var : {Gamma: Context} -> {x: Id} -> {T: Ty} -> +> Gamma x = Just T -> +> (Gamma |- (Tvar x) :: T) +> T_Abs : {Gamma: Context} -> {x: Id} -> {T11, T12: Ty} -> {t12 : Tm} -> +> ((Gamma & {{ x ==> T11 }}) |- t12 :: T12) -> +> Gamma |- (Tabs x T11 t12) :: (T11 :=> T12) +> T_App : {Gamma: Context} -> {T11, T12: Ty} -> {t1, t2 : Tm} -> +> (Gamma |- t1 :: (T11 :=> T12)) -> +> (Gamma |- t2 :: T11) -> +> Gamma |- (t1 # t2) :: T12 +> T_True : {Gamma: Context} -> +> Gamma |- Ttrue :: TBool +> T_False : {Gamma: Context} -> +> Gamma |- Tfalse :: TBool +> T_If : {Gamma: Context} -> {T : Ty} -> {t1, t2, t3 : Tm} -> +> (Gamma |- t1 :: TBool) -> +> (Gamma |- t2 :: T) -> +> (Gamma |- t3 :: T) -> +> Gamma |- (Tif t1 t2 t3) :: T + +==== Examples + +> typing_example_1 : empty |- (Tabs (MkId "x") TBool (var "x")) :: (TBool :=> TBool) +> typing_example_1 = T_Abs (T_Var Refl) + + +Another example: + +``` + empty |- \x:A. \y:A->A. y (y x) + ::A -> (A->A) -> A. +``` + +> typing_example_2 : empty |- +> (Tabs (MkId "x") TBool +> (Tabs (MkId "y") (TBool :=> TBool) +> (var "y" # var "y" # var "x"))) :: +> (TBool :=> (TBool :=> TBool) :=> TBool) +> typing_example_2 = +> T_Abs (T_Abs (T_App (T_Var Refl) (T_App (T_Var Refl) (T_Var Refl)))) + + +==== Exercise: 2 stars (typing_example_3) + +Formally prove the following typing derivation holds: + +``` + empty |- \x:Bool->B. \y:Bool->Bool. \z:Bool. + y (x z) + ::T. +``` + +> typing_example_3 : +> (T : Ty ** empty |- +> (Tabs (MkId "x") (TBool :=> TBool) +> (Tabs (MkId "y") (TBool :=> TBool) +> (Tabs (MkId "z") TBool +> (Tvar (MkId "y") # (Tvar (MkId "x") # Tvar (MkId "z")))))) :: T) +> typing_example_3 = ?typing_example_3_rhs + +$\square$ + +We can also show that terms are _not_ typable. For example, let's +formally check that there is no typing derivation assigning a type +to the term `\x:Bool. \y:Bool, x y` -- i.e., + +``` + ~ exists T, + empty |- \x:Bool. \y:Bool, x y ::T. +``` + +> forallToExistence : {X : Type} -> {P: X -> Type} -> +> ((a : X) -> Not (P a)) -> Not (a : X ** P a) +> forallToExistence hyp (a ** p2) = hyp a p2 + +> typing_nonexample_1 : +> Not (T : Ty ** +> empty |- +> (Tabs (MkId "x") TBool +> (Tabs (MkId "y") TBool +> (Tvar (MkId "x") # Tvar (MkId y)))) :: T) +> typing_nonexample_1 = forallToExistence +> (\ a , (T_Abs (T_Abs (T_App (T_Var Refl)(T_Var Refl)))) impossible) + +==== Exercise: 3 stars, optional (typing_nonexample_3) + +Another nonexample: + +``` ~ (exists S, exists T, + empty |- \x:S. x x ::T). +``` + +> typing_nonexample_3 : +> Not (s : Ty ** t : Ty ** +> empty |- +> (Tabs (MkId "x") s +> (Tvar (MkId "x") # Tvar (MkId "x"))) :: t) +> typing_nonexample_3 = ?typing_nonexample_3_rhs + +$\square$ diff --git a/src/StlcProp.lidr b/src/StlcProp.lidr new file mode 100644 index 0000000..8af6c2a --- /dev/null +++ b/src/StlcProp.lidr @@ -0,0 +1,825 @@ += StlcProp + +== StlcProp: Properties of STLC + +> module StlcProp +> import Maps +> import Stlc + +> %access public export +> %default total + +In this chapter, we develop the fundamental theory of the Simply +Typed Lambda Calculus -- in particular, the type safety +theorem. + +== Canonical Forms + +As we saw for the simple calculus in the `Types` chapter, the +first step in establishing basic properties of reduction and types +is to identify the possible _canonical forms_ (i.e., well-typed +closed values) belonging to each type. For `Bool`, these are the +boolean values `ttrue` and `tfalse`; for arrow types, they are +lambda-abstractions. + +> canonical_forms_bool : {t : Tm} -> +> (empty |- t :: TBool) -> +> Value t -> +> (t = Ttrue) `Either` (t = Tfalse) +> canonical_forms_bool {t=Ttrue} tb vt = Left Refl +> canonical_forms_bool {t=Tfalse} tb vt = Right Refl + + +> canonical_forms_fun : {t: Tm} -> {ty1, ty2: Ty} -> +> (empty |- t :: (ty1 :=> ty2)) -> +> Value t -> +> (x : Id ** u : Tm ** t = Tabs x ty1 u) +> canonical_forms_fun {t = Tabs x ty t1} {ty1} tt vt = +> case tt of +> T_Abs {x} {t12} pre => (x ** t12 ** Refl) + + +== Progress + +The _progress_ theorem tells us that closed, well-typed +terms are not stuck: either a well-typed term is a value, or it +can take a reduction step. The proof is a relatively +straightforward extension of the progress proof we saw in the +`Types` chapter. + +> progress : {t : Tm} -> {ty: Ty} -> +> ((empty {a=Ty}) |- t :: ty) -> +> (Value t) `Either` (t': Tm ** t ->> t') + +_Proof_: By induction on the derivation of `|- t :: T` + + - The last rule of the derivation cannot be `T_Var`, since a + variable is never well typed in an empty context. + + - The `T_True`, `T_False`, and `T_Abs` cases are trivial, since in + each of these cases we can see by inspecting the rule that `t` + is a value. + + - If the last rule of the derivation is `T_App`, then `t` has the + form `t1 t2` for some `t1` and `t2`, where `|- t1 :: T2 -> T` + and `|- t2 :: T2` for some type `T2`. By the induction + hypothesis, either `t1` is a value or it can take a reduction + step. + + - If `t1` is a value, then consider `t2`, which by the other + induction hypothesis must also either be a value or take a + step. + + - Suppose `t2` is a value. Since `t1` is a value with an + arrow type, it must be a lambda abstraction; hence `t1 + t2` can take a step by `ST_AppAbs`. + + - Otherwise, `t2` can take a step, and hence so can `t1 + t2` by `ST_App2`. + + - If `t1` can take a step, then so can `t1 t2` by `ST_App1`. + + - If the last rule of the derivation is `T_If`, then `t = if t1 + then t2 else t3`, where `t1` has type `Bool`. By the IH, `t1` + either is a value or takes a step. + + - If `t1` is a value, then since it has type `Bool` it must be + either `true` or `false`. If it is `true`, then `t` steps + to `t2`; otherwise it steps to `t3`. + + - Otherwise, `t1` takes a step, and therefore so does `t` (by + `ST_If`). + + +> progress {t=Tvar x} (T_Var Refl) impossible +> progress {t=Ttrue} _ = Left V_true +> progress {t=Tfalse} _ = Left V_false +> progress {t=Tabs x ty t1} _ = Left V_abs +> progress {t=tl # tr} (T_App hl hr) = +> let indHypl = progress {t=tl} hl +> in case indHypl of +> Right (t' ** step) => Right (t' # tr ** ST_App1 step) +> Left vl => +> let indHypR = progress {t=tr} hr +> in case indHypR of +> Right (t' ** step) => Right (tl # t' ** ST_App2 vl step) +> Left vr => +> case vl of +> V_abs {x} {t=tl} => Right (subst x tr tl ** ST_AppAbs vr) +> progress {t=Tif tb tp tn} (T_If hb hp hr) = +> let indHyp = progress {t=tb} hb +> in case indHyp of +> Left vl => +> case vl of +> V_true => Right (tp ** ST_IfTrue) +> V_false => Right (tn ** ST_IfFalse) +> Right (t' ** step) => Right (Tif t' tp tn ** ST_If step) + +== Preservation + +The other half of the type soundness property is the +preservation of types during reduction. For this part, we'll need +to develop some technical machinery for reasoning about variables +and substitution. Working from top to bottom (from the high-level +property we are actually interested in to the lowest-level +technical lemmas that are needed by various cases of the more +interesting proofs), the story goes like this: + + - The _preservation theorem_ is proved by induction on a typing + derivation, pretty much as we did in the `Types` chapter. + The one case that is significantly different is the one for + the `ST_AppAbs` rule, whose definition uses the substitution + operation. To see that this step preserves typing, we need to + know that the substitution itself does. So we prove a... + + - _substitution lemma_, stating that substituting a (closed) + term `s` for a variable `x` in a term `t` preserves the type + of `t`. The proof goes by induction on the form of `t` and + requires looking at all the different cases in the definition + of substitition. This time, the tricky cases are the ones for + variables and for function abstractions. In both, we discover + that we need to take a term `s` that has been shown to be + well-typed in some context `Gamma` and consider the same term + `s` in a slightly different context `Gamma'`. For this we + prove a... + + - _context invariance_ lemma, showing that typing is preserved + under "inessential changes" to the context `Gamma` -- in + particular, changes that do not affect any of the free + variables of the term. And finally, for this, we need a + careful definition of... + + - the _free variables_ in a term -- i.e., variables that are + used in the term and where these uses are _not_ in the scope of + an enclosing function abstraction binding a variable of the + same name. + +To make Idris happy, we need to formalize the story in the opposite +order... + +=== Free Occurrences + +A variable `x` _appears free in_ a term _t_ if `t` contains some +occurrence of `x` that is not under an abstraction labeled `x`. +For example: + - `y` appears free, but `x` does not, in `\x:T->U. x y` + - both `x` and `y` appear free in `(\x:T->U. x y) x` + - no variables appear free in `\x:T->U. \y:T. x y` + +Formally: + +> data Appears_free_in : Id -> Tm -> Type where +> Afi_var : {x : Id} -> +> Appears_free_in x (Tvar x) +> Afi_app1 : {x : Id} -> {t1, t2: Tm} -> +> Appears_free_in x t1 -> +> Appears_free_in x (t1 # t2) +> Afi_app2 : {x : Id} -> {t1, t2: Tm} -> +> Appears_free_in x t2 -> +> Appears_free_in x (t1 # t2) +> Afi_abs : {x,y : Id} -> {t12: Tm} -> {T11: Ty} -> +> Not (y = x) -> +> Appears_free_in x t12 -> +> Appears_free_in x (Tabs y T11 t12) +> Afi_if1 : {x : Id} -> {t1, t2, t3: Tm} -> +> Appears_free_in x t1 -> +> Appears_free_in x (Tif t1 t2 t3) +> Afi_if2 : {x : Id} -> {t1, t2, t3: Tm} -> +> Appears_free_in x t2 -> +> Appears_free_in x (Tif t1 t2 t3) +> Afi_if3 : {x : Id} -> {t1, t2, t3: Tm} -> +> Appears_free_in x t3 -> +> Appears_free_in x (Tif t1 t2 t3) + + +The _free variables_ of a term are just the variables that appear +free in it. A term with no free variables is said to be _closed_. + +> closed: Tm -> Type +> closed t = Not (x: Id ** Appears_free_in x t) + +An _open_ term is one that may contain free variables. (I.e., every +term is an open term; the closed terms are a subset of the open ones. +"Open" really means "possibly containing free variables.") + +==== Exercise: 1 star (afi) + +In the space below, write out the rules of the `appears_free_in` +relation in informal inference-rule notation. (Use whatever +notational conventions you like -- the point of the exercise is +just for you to think a bit about the meaning of each rule.) +Although this is a rather low-level, technical definition, +understanding it is crucial to understanding substitution and its +properties, which are really the crux of the lambda-calculus. + +(* FILL IN HERE *) + +=== Substitution + +To prove that substitution preserves typing, we first need a +technical lemma connecting free variables and typing contexts: If +a variable `x` appears free in a term `t`, and if we know `t` is +well typed in context `Gamma`, then it must be the case that +`Gamma` assigns a type to `x`. *) + +> free_in_context : {x : Id} -> {t: Tm} -> {ty: Ty} -> {gamma: Context} -> +> Appears_free_in x t -> +> (gamma |- t :: ty) -> +> (t' : Ty ** gamma x = Just t') + +_Proof_: We show, by induction on the proof that `x` appears free +in `t`, that, for all contexts `Gamma`, if `t` is well typed +under `Gamma`, then `Gamma` assigns some type to `x`. + + - If the last rule used is `afi_var`, then `t = x`, and from the + assumption that `t` is well typed under `Gamma` we have + immediately that `Gamma` assigns a type to `x`. + + - If the last rule used is `afi_app1`, then `t = t1 t2` and `x` + appears free in `t1`. Since `t` is well typed under `Gamma`, + we can see from the typing rules that `t1` must also be, and + the IH then tells us that `Gamma` assigns `x` a type. + + - Almost all the other cases are similar: `x` appears free in a + subterm of `t`, and since `t` is well typed under `Gamma`, we + know the subterm of `t` in which `x` appears is well typed + under `Gamma` as well, and the IH gives us exactly the + conclusion we want. + + - The only remaining case is `afi_abs`. In this case `t = + \y:T11.t12` and `x` appears free in `t12`, and we also know + that `x` is different from `y`. The difference from the + previous cases is that, whereas `t` is well typed under + `Gamma`, its body `t12` is well typed under `(Gamma & {{y==>T11}}`, + so the IH allows us to conclude that `x` is assigned some type + by the extended context `(Gamma & {{y==>T11}}`. To conclude that + `Gamma` assigns a type to `x`, we appeal to lemma + `update_neq`, noting that `x` and `y` are different + variables. *) + +> free_in_context {ty} Afi_var (T_Var h1) = (ty ** h1) +> free_in_context {t = t1 # t2} (Afi_app1 h) (T_App h1 h2) = free_in_context h h1 +> free_in_context {t = t1 # t2} (Afi_app2 h) (T_App h1 h2) = free_in_context h h2 +> free_in_context {t = Tif tb tp tn} (Afi_if1 h) (T_If h1 h2 h3) = free_in_context h h1 +> free_in_context {t = Tif tb tp tn} (Afi_if2 h) (T_If h1 h2 h3) = free_in_context h h2 +> free_in_context {t = Tif tb tp tn} (Afi_if3 h) (T_If h1 h2 h3) = free_in_context h h3 +> free_in_context {x} {gamma} {t = Tabs id ty tm} (Afi_abs h1 h2) (T_Abs h) = +> let (ty ** ih) = free_in_context h2 h +> in (ty ** rewrite (sym (update_neq {m=gamma} {v=ty} h1)) in ih) + +Next, we'll need the fact that any term `t` that is well typed in +the empty context is closed (it has no free variables). + +==== Exercise: 2 stars, optional (typable_empty__closed) + +> typable_empty__closed : {t: Tm} -> {ty : Ty} -> +> (empty |- t :: ty) -> +> closed t +> typable_empty__closed hyp = ?typable_empty__closed_rhs + +Sometimes, when we have a proof `Gamma |- t : T`, we will need to +replace `Gamma` by a different context `Gamma'`. When is it safe +to do this? Intuitively, it must at least be the case that +`Gamma'` assigns the same types as `Gamma` to all the variables +that appear free in `t`. In fact, this is the only condition that +is needed. + +> context_invariance : {gamma, gamma': Context} -> {t: Tm} -> {ty: Ty} -> +> (gamma |- t :: ty) -> +> ((x: Id) -> Appears_free_in x t -> gamma x = gamma' x) -> +> gamma' |- t :: ty + +_Proof_: By induction on the derivation of `Gamma |- t :: T`. + + - If the last rule in the derivation was `T_Var`, then `t = x` + and `Gamma x = T`. By assumption, `Gamma' x = T` as well, and + hence `Gamma' |- t :: T` by `T_Var`. + + - If the last rule was `T_Abs`, then `t = \y:T11. t12`, with `T + = T11 -> T12` and `Gamma & {{y==>T11}} |- t12 :: T12`. The + induction hypothesis is that, for any context `Gamma''`, if + `Gamma & {{y==>T11}}` and `Gamma''` assign the same types to + all the free variables in `t12`, then `t12` has type `T12` + under `Gamma''`. Let `Gamma'` be a context which agrees with + `Gamma` on the free variables in `t`; we must show `Gamma' |- + \y:T11. t12 :: T11 -> T12`. + + By `T_Abs`, it suffices to show that `Gamma' & {{y==>T11}} |- + t12 :: T12`. By the IH (setting `Gamma'' = Gamma' & + {{y:T11}}`), it suffices to show that `Gamma & {{y==>T11}}` + and `Gamma' & {{y==>T11}}` agree on all the variables that + appear free in `t12`. + + Any variable occurring free in `t12` must be either `y` or + some other variable. `Gamma & {{y==>T11}}` and `Gamma' & + {{y==>T11}}` clearly agree on `y`. Otherwise, note that any + variable other than `y` that occurs free in `t12` also occurs + free in `t = \y:T11. t12`, and by assumption `Gamma` and + `Gamma'` agree on all such variables; hence so do `Gamma & + {{y==>T11}}` and `Gamma' & {{y==>T11}}`. + + - If the last rule was `T_App`, then `t = t1 t2`, with `Gamma |- + t1 :: T2 -> T` and `Gamma |- t2 :: T2`. One induction + hypothesis states that for all contexts `Gamma'`, if `Gamma'` + agrees with `Gamma` on the free variables in `t1`, then `t1` + has type `T2 -> T` under `Gamma'`; there is a similar IH for + `t2`. We must show that `t1 t2` also has type `T` under + `Gamma'`, given the assumption that `Gamma'` agrees with + `Gamma` on all the free variables in `t1 t2`. By `T_App`, it + suffices to show that `t1` and `t2` each have the same type + under `Gamma'` as under `Gamma`. But all free variables in + `t1` are also free in `t1 t2`, and similarly for `t2`; hence + the desired result follows from the induction hypotheses. *) + +> context_invariance T_True freeEq = T_True +> context_invariance T_False freeEq = T_False +> context_invariance {t= Tvar id} (T_Var h) freeEq = +> let hyp = freeEq id (Afi_var {x=id}) +> in T_Var (rewrite sym hyp in h) +> context_invariance {gamma'} {t = Tabs id ty tm} (T_Abs h) freeEq = ?context_invariance_rhs +> context_invariance {gamma} {gamma'} {t = tl # tr} (T_App tyl tyr) freeEq = ?context_invariance_rhs2 +> context_invariance {t = Tif cond pos neg} (T_If condt post negt) freeEq = +> let -- dhyp = Afi_if1 {t1 =cond} {t2 = pos} {t3= neg} ?hyp1 +> hypCond = context_invariance {t=cond} condt _ +> hypPos = context_invariance {t=pos} post ?hypPos +> hypNeg = context_invariance {t=neg} negt ?hypNeg +> in T_If hypCond hypPos hypNeg + +Now we come to the conceptual heart of the proof that reduction +preserves types -- namely, the observation that _substitution_ +preserves types. + +Formally, the so-called _substitution lemma_ says this: +Suppose we have a term `t` with a free variable `x`, and suppose +we've assigned a type `T` to `t` under the assumption that `x` has +some type `U`. Also, suppose that we have some other term `v` and +that we've shown that `v` has type `U`. Then, since `v` satisfies +the assumption we made about `x` when typing `t`, we can +substitute `v` for each of the occurrences of `x` in `t` and +obtain a new term that still has type `T`. + +_Lemma_: If `Gamma & {{x==>U}} |- t :: T` and `|- v :: U`, + then `Gamma |- [x:=v]t :: T` . + +> substitution_preserves_typing : {gamma: Context} -> {x: Id} -> {t, v : Tm} -> {uty, tty: Ty} -> +> ((gamma & {{x ==> uty}}) |- t :: tty) -> +> (empty |- v :: uty) -> +> gamma |- ([x:=v] t) :: tty +> substitution_preserves_typing {x} {t=Tvar id} (T_Var st1) st2 with (decEq x id) +> | Yes prf = let af = 0 -- \ id af => +> in ?hole0 -- context_invariance st2 ?hole00 +> | No contra = let hyp = 0 -- update_neq {v} contra +> in ?hole1 +> substitution_preserves_typing st1 st2 = ?substitution_preserves_typing_rhs + +(One technical subtlety in the statement of the lemma is that +we assume `v` has type `U` in the _empty_ context -- in other +words, we assume `v` is closed. This assumption considerably +simplifies the `T_Abs` case of the proof (compared to assuming +`Gamma |- v :: U`, which would be the other reasonable assumption +at this point) because the context invariance lemma then tells us +that `v` has type `U` in any context at all -- we don't have to +worry about free variables in `v` clashing with the variable being +introduced into the context by `T_Abs`. + +The substitution lemma can be viewed as a kind of commutation +property. Intuitively, it says that substitution and typing can +be done in either order: we can either assign types to the terms +`t` and `v` separately (under suitable contexts) and then combine +them using substitution, or we can substitute first and then +assign a type to ` [x:=v] t ` -- the result is the same either +way. + +_Proof_: We show, by induction on `t`, that for all `T` and +`Gamma`, if `Gamma & {{x==>U}} |- t :: T` and `|- v :: U`, then +`Gamma |- [x:=v] t :: T`. + + - If `t` is a variable there are two cases to consider, + depending on whether `t` is `x` or some other variable. + + - If `t = x`, then from the fact that `Gamma & {{x==>U}} |- + x :: T` we conclude that `U = T`. We must show that + `[x:=v]x = v` has type `T` under `Gamma`, given the + assumption that `v` has type `U = T` under the empty + context. This follows from context invariance: if a + closed term has type `T` in the empty context, it has that + type in any context. + + - If `t` is some variable `y` that is not equal to `x`, then + we need only note that `y` has the same type under `Gamma + & {{x==>U}}` as under `Gamma`. + + - If `t` is an abstraction `\y:T11. t12`, then the IH tells us, + for all `Gamma'` and `T'`, that if `Gamma' & {{x==>U} |- t12 + :: T'` and `|- v :: U`, then `Gamma' |- [x:=v] t12 :: T'`. + + The substitution in the conclusion behaves differently + depending on whether `x` and `y` are the same variable. + + First, suppose `x = y`. Then, by the definition of + substitution, `[x:=v]t = t`, so we just need to show `Gamma |- + t :: T`. But we know `Gamma & {{x==>U}} |- t : T`, and, + since `y` does not appear free in `\y:T11. t12`, the context + invariance lemma yields `Gamma |- t :: T`. + + Second, suppose `x <> y`. We know `Gamma & {{x==>U; y==>T11}} + |- t12 :: T12` by inversion of the typing relation, from + which `Gamma & {{y==>T11; x==>U}} |- t12 :: T12` follows by + the context invariance lemma, so the IH applies, giving us + `Gamma & {{y==>T11}} |- [x:=v]t12 :: T12`. By `T_Abs`, + `Gamma |- \y:T11. [x:=v]t12 :: T11->T12`, and by the + definition of substitution (noting that `x <> y`), `Gamma |- + \y:T11. [x:=v]t12 :: T11->T12` as required. + + - If `t` is an application `t1 t2`, the result follows + straightforwardly from the definition of substitution and the + induction hypotheses. + + - The remaining cases are similar to the application case. + +_Technical note_: This proof is a rare case where an induction on +terms, rather than typing derivations, yields a simpler argument. +The reason for this is that the assumption `Gamma & {{x==>U}} |- t +:: T` is not completely generic, in the sense that one of the +"slots" in the typing relation -- namely the context -- is not +just a variable, and this means that Coq's native induction tactic +does not give us the induction hypothesis that we want. It is +possible to work around this, but the needed generalization is a +little tricky. The term `t`, on the other hand, is completely +generic. + +Proof with eauto. + intros Gamma x U t v T Ht Ht'. + generalize dependent Gamma. generalize dependent T. + induction t; intros T Gamma H; + (* in each case, we'll want to get at the derivation of H *) + inversion H; subst; simpl... + - (* tvar *) + rename s into y. destruct (beq_stringP x y) as `Hxy|Hxy`. + + (* x=y *) + subst. + rewrite update_eq in H2. + inversion H2; subst. + eapply context_invariance. eassumption. + apply typable_empty__closed in Ht'. unfold closed in Ht'. + intros. apply (Ht' x0) in H0. inversion H0. + + (* x<>y *) + apply T_Var. rewrite update_neq in H2... + - (* tabs *) + rename s into y. rename t into T. apply T_Abs. + destruct (beq_stringP x y) as `Hxy | Hxy`. + + (* x=y *) + subst. rewrite update_shadow in H5. apply H5. + + (* x<>y *) + apply IHt. eapply context_invariance... + intros z Hafi. unfold update, t_update. + destruct (beq_stringP y z) as `Hyz | Hyz`; subst; trivial. + rewrite <- beq_string_false_iff in Hxy. + rewrite Hxy... +Qed. + +=== Main Theorem + +We now have the tools we need to prove preservation: if a closed +term `t` has type `T` and takes a step to `t'`, then `t'` +is also a closed term with type `T`. In other words, the small-step +reduction relation preserves types. + +> preservation : {t, t' : Tm} -> {ty: Ty} -> +> (empty |- t :: ty) -> +> t ->> t' -> +> empty |- t' :: ty + +_Proof_: By induction on the derivation of `|- t :: T`. + + - We can immediately rule out `T_Var`, `T_Abs`, `T_True`, and + `T_False` as the final rules in the derivation, since in each of + these cases `t` cannot take a step. + + - If the last rule in the derivation is `T_App`, then `t = t1 + t2`. There are three cases to consider, one for each rule that + could be used to show that `t1 t2` takes a step to `t'`. + + - If `t1 t2` takes a step by `ST_App1`, with `t1` stepping to + `t1'`, then by the IH `t1'` has the same type as `t1`, and + hence `t1' t2` has the same type as `t1 t2`. + + - The `ST_App2` case is similar. + + - If `t1 t2` takes a step by `ST_AppAbs`, then `t1 = + \x:T11.t12` and `t1 t2` steps to ``x:=t2`t12`; the + desired result now follows from the fact that substitution + preserves types. + + - If the last rule in the derivation is `T_If`, then `t = if t1 + then t2 else t3`, and there are again three cases depending on + how `t` steps. + + - If `t` steps to `t2` or `t3`, the result is immediate, since + `t2` and `t3` have the same type as `t`. + + - Otherwise, `t` steps by `ST_If`, and the desired conclusion + follows directly from the induction hypothesis. *) + +> preservation {t= lt # rt} (T_App tal tar) (ST_App1 red) = +> let indHyp = preservation {t=lt} tal red +> in T_App indHyp tar +> preservation {t= lt # rt} (T_App tal tar) (ST_App2 val red) = +> let indHyp = preservation {t=rt} tar red +> in T_App tal indHyp +> preservation {t= (Tabs x ty lt) # rt} (T_App (T_Abs tabs) tar) (ST_AppAbs val) = +> substitution_preserves_typing {x} {t=lt} {v=rt} tabs tar +> preservation {t= Tif cond pos neg} (T_If condht posht neght) (ST_If val) = +> let indHyp = preservation {t=cond} condht val +> in T_If indHyp posht neght +> preservation {t= Tif Ttrue pos neg} (T_If condht posht neght) ST_IfTrue = posht +> preservation {t= Tif Tfalse pos neg} (T_If condht posht neght) ST_IfFalse = neght + +==== Exercise: 2 stars, recommended (subject_expansion_stlc) + +An exercise in the `Types` chapter asked about the _subject +expansion_ property for the simple language of arithmetic and +boolean expressions. Does this property hold for STLC? That is, +is it always the case that, if `t ==> t'` and `has_type t' T`, +then `empty |- t :: T`? If so, prove it. If not, give a +counter-example not involving conditionals. + +You can state your counterexample informally +in words, with a brief explanation. + +(* FILL IN HERE *) + + + +(* ################################################################# *) +(** * Type Soundness *) + +(** **** Exercise: 2 stars, optional (type_soundness) *) +(** Put progress and preservation together and show that a well-typed + term can _never_ reach a stuck state. *) + +Definition stuck (t:tm) : Prop := + (normal_form step) t /\ ~ value t. + +Corollary soundness : forall t t' T, + empty |- t :: T -> + t ==>* t' -> + ~(stuck t'). +Proof. + intros t t' T Hhas_type Hmulti. unfold stuck. + intros `Hnf Hnot_val`. unfold normal_form in Hnf. + induction Hmulti. + (* FILL IN HERE *) Admitted. +(** `` *) + +(* ################################################################# *) +(** * Uniqueness of Types *) + +(** **** Exercise: 3 stars (types_unique) *) +(** Another nice property of the STLC is that types are unique: a + given term (in a given context) has at most one type. *) +(** Formalize this statement as a theorem called + `unique_types`, and prove your theorem. *) + +(* FILL IN HERE *) +(** `` *) + +(* ################################################################# *) +(** * Additional Exercises *) + +(** **** Exercise: 1 star (progress_preservation_statement) *) +(** Without peeking at their statements above, write down the progress + and preservation theorems for the simply typed lambda-calculus (as + Coq theorems). + You can write `Admitted` for the proofs. *) +(* FILL IN HERE *) +(** `` *) + +(** **** Exercise: 2 stars (stlc_variation1) *) +(** Suppose we add a new term `zap` with the following reduction rule + + --------- (ST_Zap) + t ==> zap + +and the following typing rule: + + ---------------- (T_Zap) + Gamma |- zap : T + + Which of the following properties of the STLC remain true in + the presence of these rules? For each property, write either + "remains true" or "becomes false." If a property becomes + false, give a counterexample. + + - Determinism of `step` +(* FILL IN HERE *) + - Progress +(* FILL IN HERE *) + - Preservation +(* FILL IN HERE *) +*) +(** `` *) + +(** **** Exercise: 2 stars (stlc_variation2) *) +(** Suppose instead that we add a new term `foo` with the following + reduction rules: + + ----------------- (ST_Foo1) + (\x:A. x) ==> foo + + ------------ (ST_Foo2) + foo ==> true + + Which of the following properties of the STLC remain true in + the presence of this rule? For each one, write either + "remains true" or else "becomes false." If a property becomes + false, give a counterexample. + + - Determinism of `step` +(* FILL IN HERE *) + - Progress +(* FILL IN HERE *) + - Preservation +(* FILL IN HERE *) +*) +(** `` *) + +(** **** Exercise: 2 stars (stlc_variation3) *) +(** Suppose instead that we remove the rule `ST_App1` from the `step` + relation. Which of the following properties of the STLC remain + true in the presence of this rule? For each one, write either + "remains true" or else "becomes false." If a property becomes + false, give a counterexample. + + - Determinism of `step` +(* FILL IN HERE *) + - Progress +(* FILL IN HERE *) + - Preservation +(* FILL IN HERE *) +*) +(** `` *) + +(** **** Exercise: 2 stars, optional (stlc_variation4) *) +(** Suppose instead that we add the following new rule to the + reduction relation: + + ---------------------------------- (ST_FunnyIfTrue) + (if true then t1 else t2) ==> true + + Which of the following properties of the STLC remain true in + the presence of this rule? For each one, write either + "remains true" or else "becomes false." If a property becomes + false, give a counterexample. + + - Determinism of `step` +(* FILL IN HERE *) + - Progress +(* FILL IN HERE *) + - Preservation +(* FILL IN HERE *) +*) +(** `` *) + +(** **** Exercise: 2 stars, optional (stlc_variation5) *) +(** Suppose instead that we add the following new rule to the typing + relation: + + Gamma |- t1 :: Bool->Bool->Bool + Gamma |- t2 :: Bool + ------------------------------ (T_FunnyApp) + Gamma |- t1 t2 :: Bool + + Which of the following properties of the STLC remain true in + the presence of this rule? For each one, write either + "remains true" or else "becomes false." If a property becomes + false, give a counterexample. + + - Determinism of `step` +(* FILL IN HERE *) + - Progress +(* FILL IN HERE *) + - Preservation +(* FILL IN HERE *) +*) +(** `` *) + +(** **** Exercise: 2 stars, optional (stlc_variation6) *) +(** Suppose instead that we add the following new rule to the typing + relation: + + Gamma |- t1 :: Bool + Gamma |- t2 :: Bool + --------------------- (T_FunnyApp') + Gamma |- t1 t2 :: Bool + + Which of the following properties of the STLC remain true in + the presence of this rule? For each one, write either + "remains true" or else "becomes false." If a property becomes + false, give a counterexample. + + - Determinism of `step` +(* FILL IN HERE *) + - Progress +(* FILL IN HERE *) + - Preservation +(* FILL IN HERE *) +*) +(** `` *) + +(** **** Exercise: 2 stars, optional (stlc_variation7) *) +(** Suppose we add the following new rule to the typing relation + of the STLC: + + ------------------- (T_FunnyAbs) + |- \x:Bool.t :: Bool + + Which of the following properties of the STLC remain true in + the presence of this rule? For each one, write either + "remains true" or else "becomes false." If a property becomes + false, give a counterexample. + + - Determinism of `step` +(* FILL IN HERE *) + - Progress +(* FILL IN HERE *) + - Preservation +(* FILL IN HERE *) +*) +(** `` *) + +End STLCProp. + +(* ================================================================= *) +(** ** Exercise: STLC with Arithmetic *) + +(** To see how the STLC might function as the core of a real + programming language, let's extend it with a concrete base + type of numbers and some constants and primitive + operators. *) + +Module STLCArith. +Import STLC. + +(** To types, we add a base type of natural numbers (and remove + booleans, for brevity). *) + +Inductive ty : Type := + | TArrow : ty -> ty -> ty + | TNat : ty. + +(** To terms, we add natural number constants, along with + successor, predecessor, multiplication, and zero-testing. *) + +Inductive tm : Type := + | tvar : string -> tm + | tapp : tm -> tm -> tm + | tabs : string -> ty -> tm -> tm + | tnat : nat -> tm + | tsucc : tm -> tm + | tpred : tm -> tm + | tmult : tm -> tm -> tm + | tif0 : tm -> tm -> tm -> tm. + +(** **** Exercise: 4 stars (stlc_arith) *) +(** Finish formalizing the definition and properties of the STLC + extended with arithmetic. This is a longer exercise. Specifically: + + 1. Copy the core definitions for STLC that we went through, + as well as the key lemmas and theorems, and paste them + into the file at this point. Do not copy examples, exercises, + etc. (In particular, make sure you don't copy any of the `` + comments at the end of exercises, to avoid confusing the + autograder.) + + You should copy over five definitions: + - Fixpoint susbt + - Inductive value + - Inductive step + - Inductive has_type + - Inductive appears_free_in + + And five theorems, with their proofs: + - Lemma context_invariance + - Lemma free_in_context + - Lemma substitution_preserves_typing + - Theorem preservation + - Theorem progress + + It will be helpful to also copy over "Reserved Notation", + "Notation", and "Hint Constructors" for these things. + + 2. Edit and extend the five definitions (subst, value, step, + has_type, and appears_free_in) so they are appropriate + for the new STLC extended with arithmetic. + + 3. Extend the proofs of all the five properties of the original + STLC to deal with the new syntactic forms. Make sure Coq + accepts the whole file. *) + +(* FILL IN HERE *) +(** `` *) + +End STLCArith. + +(** $Date$ *) diff --git a/src/Types.lidr b/src/Types.lidr new file mode 100644 index 0000000..026a14f --- /dev/null +++ b/src/Types.lidr @@ -0,0 +1,791 @@ += Types + +== Types: Type Systems + +> module Types +> import Smallstep +> %hide Smallstep.(->>) +> %hide Smallstep.Tm +> %hide Smallstep.Ttrue +> %hide Smallstep.Tfalse + + + +> %access public export +> %default total + + +Our next major topic is _type systems_ -- static program +analyses that classify expressions according to the "shapes" of +their results. We'll begin with a typed version of the simplest +imaginable language, to introduce the basic ideas of types and +typing rules and the fundamental theorems about type systems: +_type preservation_ and _progress_. In chapter `Stlc` we'll move +on to the _simply typed lambda-calculus_, which lives at the core +of every modern functional programming language (including +Idris!). + +== Typed Arithmetic Expressions + +To motivate the discussion of type systems, let's begin as +usual with a tiny toy language. We want it to have the potential +for programs to go wrong because of runtime type errors, so we +need something a tiny bit more complex than the language of +constants and addition that we used in chapter `Smallstep`: a +single kind of data (e.g., numbers) is too simple, but just two +kinds (numbers and booleans) gives us enough material to tell an +interesting story. + +The language definition is completely routine. + +=== Syntax + +Here is the syntax, informally: + +``` + t ::= true + | false + | if t then t else t + | 0 + | succ t + | pred t + | iszero t +``` + +And here it is formally: + +> data Tm : Type where +> Ttrue : Tm +> Tfalse : Tm +> Tif : Tm -> Tm -> Tm -> Tm +> Tzero : Tm +> Tsucc : Tm -> Tm +> Tpred : Tm -> Tm +> Tiszero : Tm -> Tm + +_Values_ are `true`, `false`, and numeric values... + +> data Bvalue : Tm -> Type where +> Bv_true : Bvalue Ttrue +> Bv_false : Bvalue Tfalse +> +> data Nvalue : Tm -> Type where +> Nv_zero : Nvalue Tzero +> Nv_succ : {t: Tm} -> Nvalue t -> Nvalue (Tsucc t) +> +> data Value : Tm -> Type where +> V_bool : Bvalue t -> Value t +> V_nat : Nvalue t -> Value t + +=== Operational Semantics + +Here is the single-step relation, first informally... + +\[ + \begin{prooftree} + \infer0[\idr{ST_IfTrue}]{\idr{if true then t1 else t2 ->> t1}} + \end{prooftree} + \newline +\] + +\[ + \begin{prooftree} + \infer0[\idr{ST_IfFalse}]{\idr{if false then t1 else t2 ->> t2}} + \end{prooftree} + \newline +\] + +\[ + \begin{prooftree} + \hypo{\idr{t1 ->> t1'}} + \infer1[\idr{ST_If}]{\idr{if t1 then t2 else t3 ->> if t1' then t2 else t3}} + \end{prooftree} +\] + +\[ + \begin{prooftree} + \hypo{\idr{t1 ->> t1'}} + \infer1[\idr{ST_Succ}]{\idr{succ t1 ->> succ t1'}} + \end{prooftree} +\] + +\[ + \begin{prooftree} + \infer0[\idr{ST_PredZero}]{\idr{pred 0 ->> 0}} + \end{prooftree} + \newline +\] + +\[ + \begin{prooftree} + \hypo{\idr{numeric value v1}} + \infer1[\idr{ST_PredSucc}]{\idr{pred (succ v1) ->> v1}} + \end{prooftree} +\] + +\[ + \begin{prooftree} + \hypo{\idr{t1 ->> t1'}} + \infer1[\idr{ST_Pred}]{\idr{pred t1 ->> pred t1'}} + \end{prooftree} +\] + +\[ + \begin{prooftree} + \infer0[\idr{ST_IszeroZero}]{\idr{iszero 0 ->> true}} + \end{prooftree} + \newline +\] + +\[ + \begin{prooftree} + \hypo{\idr{numeric value v1}} + \infer1[\idr{ST_IszeroSucc}]{\idr{iszero (succ v1) ->> false}} + \end{prooftree} +\] + +\[ + \begin{prooftree} + \hypo{\idr{t1 ->> t1'}} + \infer1[\idr{ST_Iszero}]{\idr{iszero t1 ->> iszero t1'}} + \end{prooftree} +\] + +... and then formally: + + +> mutual +> infixl 6 ->> +> (->>) : Tm -> Tm -> Type +> (->>) = Types.Step +> +> data Step : Tm -> Tm -> Type where +> ST_IfTrue : {t1, t2: Tm} -> Tif Ttrue t1 t2 ->> t1 +> ST_IfFalse : {t1, t2: Tm} -> Tif Tfalse t1 t2 ->> t2 +> ST_If : {t1, t2, t3, t1': Tm} -> t1 ->> t1' -> Tif t1 t2 t3 ->> Tif t1' t2 t3 +> ST_Succ : {t1, t1': Tm} -> t1 ->> t1' -> Tsucc t1 ->> Tsucc t1' +> ST_PredZero : Tpred tzero ->> tzero +> ST_PredSucc : {t1 :Tm} -> Nvalue t1 -> Tpred (Tsucc t1) ->> t1 +> ST_Pred : {t1, t1': Tm} -> t1 ->> t1' -> Tpred t1 ->> Tpred t1' +> ST_IszeroZero : Tiszero Tzero ->> Ttrue +> ST_IszeroSucc : {t1: Tm} -> Nvalue t1 -> Tiszero (Tsucc t1) ->> Tfalse +> ST_Iszero : {t1, t1': Tm} -> t1 ->> t1' -> Tiszero t1 ->> Tiszero t1' + + +Notice that the `step` relation doesn't care about whether +expressions make global sense -- it just checks that the operation +in the _next_ reduction step is being applied to the right kinds +of operands. For example, the term `succ true` (i.e., +`tsucc ttrue` in the formal syntax) cannot take a step, but the +almost as obviously nonsensical term + + succ (if true then true else true) + +can take a step (once, before becoming stuck). + +=== Normal Forms and Values + +The first interesting thing to notice about this `step` relation +is that the strong progress theorem from the `Smallstep` chapter +fails here. That is, there are terms that are normal forms (they +can't take a step) but not values (because we have not included +them in our definition of possible "results of reduction"). Such +terms are _stuck_. + +> step_normal_form : (t : Tm) -> Type +> step_normal_form = normal_form Types.Step + +> stuck : (t : Tm) -> Type +> stuck t = (step_normal_form t, Not (Value t)) + +==== Exercise: 2 stars (some_term_is_stuck) + +> some_term_is_stuck : (t ** stuck t) +> some_term_is_stuck = ?some_term_is_stuck_rhs + +$\square$ + +However, although values and normal forms are _not_ the same in this +language, the set of values is included in the set of normal +forms. This is important because it shows we did not accidentally +define things so that some value could still take a step. + +==== Exercise: 3 stars (value_is_nf) + +> value_is_nf : {t: Tm} -> Value t -> step_normal_form t +> value_is_nf = ?value_is_nf_rhs + +$\square$ + +==== Exercise: 3 stars, optional (step_deterministic) + +Use `value_is_nf` to show that the `step` relation is also + deterministic. + +> step_deterministic : deterministic step +> step_deterministic = ?step_deterministic_rhs + +$\square$ + +== Typing + +The next critical observation is that, although this +language has stuck terms, they are always nonsensical, mixing +booleans and numbers in a way that we don't even _want_ to have a +meaning. We can easily exclude such ill-typed terms by defining a +_typing relation_ that relates terms to the types (either numeric +or boolean) of their final results. + +> data Ty : Type where +> TBool : Ty +> TNat : Ty + +In informal notation, the typing relation is often written +`|- t \in T` and pronounced "`t` has type `T`." The `|-` symbol +is called a "turnstile." Below, we're going to see richer typing +relations where one or more additional "context" arguments are +written to the left of the turnstile. For the moment, the context +is always empty. + +\[ + \begin{prooftree} + \infer0[\idr{T_True}]{\idr{|- true \\in Bool}} + \end{prooftree} + \newline +\] + +\[ + \begin{prooftree} + \infer0[\idr{T_False}]{\idr{|- false \\in Bool}} + \end{prooftree} + \newline +\] + +\[ + \begin{prooftree} + \hypo{\idr{|- t1 \\in Bool}} + \hypo{\idr{|- t2 \\in T}} + \hypo{\idr{|- t3 \\in T}} + \infer3[\idr{T_If}]{\idr{|- if t1 then t2 else t3 \\in T}} + \end{prooftree} + \newline +\] + +\[ + \begin{prooftree} + \infer0[\idr{T_Zero}]{\idr{|- 0 \\in Nat}} + \end{prooftree} + \newline +\] + +\[ + \begin{prooftree} + \hypo{\idr{|- t1 \\in Nat}} + \infer1[\idr{T_Succ}]{\idr{|- succ t1 \\in Nat}} + \end{prooftree} + \newline +\] + +\[ + \begin{prooftree} + \hypo{\idr{|- t1 \\in Nat}} + \infer1[\idr{T_Pred}]{\idr{|- pred t1 \\in Nat}} + \end{prooftree} + \newline +\] + +\[ + \begin{prooftree} + \hypo{\idr{|- t1 \\in Nat}} + \infer1[\idr{T_IsZero}]{\idr{|- iszero t1 \\in Bool}} + \end{prooftree} + \newline +\] + +> syntax "|-" [p] ":" [q] "."= Has_type p q + +> data Has_type : Tm -> Ty -> Type where +> T_True : |- Ttrue : TBool . +> T_False : |- Tfalse : TBool . +> T_If : {t1, t2, t3: Tm} -> {T: Ty} -> +> |- t1 : TBool . -> +> |- t2 : T . -> +> |- t3 : T . -> +> |- (Tif t1 t2 t3) : T . +> T_Zero : |- Tzero : TNat . +> T_Succ : {t1 : Tm} -> +> |- t1 : TNat . -> +> |- (Tsucc t1) : TNat . +> T_Pred : {t1 : Tm} -> +> |- t1 : TNat . -> +> |- (Tpred t1) : TNat . +> T_Iszero : {t1 : Tm} -> +> |- t1 : TNat . -> +> |- (Tiszero t1) : TBool . + +> has_type_1 : |- (Tif Tfalse Tzero (Tsucc Tzero)) : TNat . +> has_type_1 = T_If (T_False) (T_Zero) (T_Succ T_Zero) + +It's important to realize that the typing relation is a +_conservative_ (or _static_) approximation: it does not consider +what happens when the term is reduced -- in particular, it does +not calculate the type of its normal form. + +> has_type_not : Not ( |- (Tif Tfalse Tzero Ttrue) : TBool . ) +> has_type_not (T_If (T_False) (T_Zero) (T_True)) impossible + +==== Exercise: 1 star, optional (succ_hastype_nat__hastype_nat) + +> succ_hastype_nat__hastype_nat : {t : Tm} -> +> |- (Tsucc t) : TNat . -> |- t : TNat . +> succ_hastype_nat__hastype_nat = ?succ_hastype_nat__hastype_nat_rhs + +$\square$ + +=== Canonical forms + +The following two lemmas capture the fundamental property that the +definitions of boolean and numeric values agree with the typing +relation. + +> bool_canonical : {t: Tm} -> |- t : TBool . -> Value t -> Bvalue t +> bool_canonical {t} ht v = +> case v of +> V_bool b => b +> V_nat n => void (lemma n ht) +> where lemma : {t:Tm} -> Nvalue t -> Not ( |- t : TBool . ) +> lemma {t=Tzero} n T_Zero impossible +> lemma {t=Tsucc n'} n (T_Succ n') impossible + +> nat_canonical : {t: Tm} -> |- t : TNat . -> Value t -> Nvalue t +> nat_canonical {t} ht v = +> case v of +> V_nat n => n +> V_bool b => void (lemma b ht) +> where lemma : {t:Tm} -> Bvalue t -> Not ( |- t : TNat . ) +> lemma {t=Ttrue} n T_True impossible +> lemma {t=Tfalse} n T_False impossible + +=== Progress + +The typing relation enjoys two critical properties. The first is +that well-typed normal forms are not stuck -- or conversely, if a +term is well typed, then either it is a value or it can take at +least one step. We call this _progress_. + +> progress : {t: Tm} -> {ty: Ty} -> |- t : ty . -> Either (Value t) (t' ** t ->> t') + +==== Exercise: 3 stars (finish_progress) + +Complete the formal proof of the `progress` property. (Make sure + you understand the parts we've given of the informal proof in the + following exercise before starting -- this will save you a lot of + time.) + +> progress {t=Tif t1 t2 t3} (T_If h1 h2 h3) = +> case progress h1 of +> Left hypL => Right ( +> let h1 = bool_canonical h1 hypL +> in case t1 of +> Ttrue => (t2 ** ST_IfTrue) +> Tfalse => (t3 ** ST_IfFalse) +> ) +> Right (t' ** hr) => Right ((Tif t' t2 t3) ** ST_If hr) +> progress t = ?progress_rhs + +$\square$ + +==== Exercise: 3 stars, advanced (finish_progress_informal) + +Complete the corresponding informal proof: + +_Theorem_: If `|- t \in T`, then either `t` is a value or else + `t ==> t'` for some `t'`. + +_Proof_: By induction on a derivation of `|- t \in T`. + +- If the last rule in the derivation is `T_If`, then `t = if t1 + then t2 else t3`, with `|- t1 \in Bool`, `|- t2 \in T` and `|- t3 + \in T`. By the IH, either `t1` is a value or else `t1` can step + to some `t1'`. + + - If `t1` is a value, then by the canonical forms lemmas + and the fact that `|- t1 \in Bool` we have that `t1` + is a `bvalue` -- i.e., it is either `true` or `false`. + If `t1 = true`, then `t` steps to `t2` by `ST_IfTrue`, + while if `t1 = false`, then `t` steps to `t3` by + `ST_IfFalse`. Either way, `t` can step, which is what + we wanted to show. + + - If `t1` itself can take a step, then, by `ST_If`, so can + `t`. + +$\square$ + +This theorem is more interesting than the strong progress theorem +that we saw in the `Smallstep` chapter, where _all_ normal forms +were values. Here a term can be stuck, but only if it is ill +typed. + + +=== Type Preservation + +The second critical property of typing is that, when a well-typed +term takes a step, the result is also a well-typed term. + +> preservation : {t, t': Tm} -> {T: Ty} -> +> |- t : T . -> t ->> t' -> |- t' : T . + +==== Exercise: 2 stars (finish_preservation) + +> preservation {t=Tif t1 t2 t3} {t'} (T_If h1 h2 h3) he = +> case he of +> ST_IfTrue => h2 +> ST_IfFalse => h3 +> ST_If hyp => +> let indHyp = preservation h1 hyp +> in T_If indHyp h2 h3 +> ST_Succ hyp impossible +> ST_PredZero impossible +> ST_PredSucc hyp impossible +> ST_Pred hyp impossible +> ST_IszeroZero impossible +> ST_IszeroSucc hyp impossible +> ST_Iszero hyp impossible +> preservation t he = ?preservation_rhs + +Complete the formal proof of the `preservation` property. (Again, + make sure you understand the informal proof fragment in the + following exercise first.) + +$\square$ + +==== Exercise: 3 stars, advanced (finish_preservation_informal) + +Complete the following informal proof: + +_Theorem_: If `|- t \in T` and `t ==> t'`, then `|- t' \in T`. + +_Proof_: By induction on a derivation of `|- t \in T`. + +- If the last rule in the derivation is `T_If`, then `t = if t1 + then t2 else t3`, with `|- t1 \in Bool`, `|- t2 \in T` and `|- t3 + \in T`. + + Inspecting the rules for the small-step reduction relation and + remembering that `t` has the form `if ...`, we see that the + only ones that could have been used to prove `t ==> t'` are + `ST_IfTrue`, `ST_IfFalse`, or `ST_If`. + + - If the last rule was `ST_IfTrue`, then `t' = t2`. But we + know that `|- t2 \in T`, so we are done. + + - If the last rule was `ST_IfFalse`, then `t' = t3`. But we + know that `|- t3 \in T`, so we are done. + + - If the last rule was `ST_If`, then `t' = if t1' then t2 + else t3`, where `t1 ==> t1'`. We know `|- t1 \in Bool` so, + by the IH, `|- t1' \in Bool`. The `T_If` rule then gives us + `|- if t1' then t2 else t3 \in T`, as required. + +$\square$ + +==== Exercise: 3 stars (preservation_alternate_proof) + +Now prove the same property again by induction on the +_evaluation_ derivation instead of on the typing derivation. +Begin by carefully reading and thinking about the first few +lines of the above proofs to make sure you understand what +each one is doing. The set-up for this proof is similar, but +not exactly the same. + +> preservation' : {t, t': Tm} -> {T: Ty} -> +> |- t : T . -> t ->> t' -> |- t' : T . +> preservation' h1 h2 = ?preservation'_rhs + +$\square$ + +The preservation theorem is often called _subject reduction_, +because it tells us what happens when the "subject" of the typing +relation is reduced. This terminology comes from thinking of +typing statements as sentences, where the term is the subject and +the type is the predicate. + +=== Type Soundness + +Putting progress and preservation together, we see that a +well-typed term can never reach a stuck state. + +> mutual +> infixl 6 ->>* +> (->>*) : Tm -> Tm -> Type +> (->>*) = multistep + +> multistep : Tm -> Tm -> Type +> multistep = Multi Step + +> soundness : {t, t': Tm} -> {T: Ty} -> +> |- t : T . -> +> t ->>* t' -> +> Not (stuck t') +> soundness ht Multi_refl (sl,sr) = +> case progress ht of +> Left hl => sr hl +> Right hr => sl hr +> soundness ht (Multi_step single multi) stuck = +> let ht' = preservation ht single +> indHyp = soundness ht' multi +> in indHyp stuck + + + +=== Additional Exercises + +==== Exercise: 2 stars, recommended (subject_expansion) + +Having seen the subject reduction property, one might +wonder whether the opposity property -- subject _expansion_ -- +also holds. That is, is it always the case that, if `t ==> t'` +and `|- t' \in T`, then `|- t \in T`? If so, prove it. If +not, give a counter-example. (You do not need to prove your +counter-example in Idris, but feel free to do so.) + +$\square$ + +==== Exercise: 2 stars (variation1) + +Suppose, that we add this new rule to the typing relation: + +```idris + T_SuccBool : {t: Tm} -> + HasType t TBool -> + |- Tsucc t . TBool +``` + +Which of the following properties remain true in the presence of +this rule? For each one, write either "remains true" or +else "becomes false." If a property becomes false, give a +counterexample. + - Determinism of `step` + + - Progress + + - Preservation + +$\square$ + +==== Exercise: 2 stars (variation2) + +Suppose, instead, that we add this new rule to the `step` relation: + +```idris + ST_Funny1 : {t2, t3: Tm} -> + (tif ttrue t2 t3) ->>* t3 +``` + +Which of the above properties become false in the presence of +this rule? For each one that does, give a counter-example. + +$\square$ + +==== Exercise: 2 stars, optional (variation3) + +Suppose instead that we add this rule: + +```idris + ST_Funny2 : {t1, t2, t2', t3: Tm} -> + t2 ->>* t2' -> + (tif t1 t2 t3) ->>* (tif t1 t2' t3) +``` + +Which of the above properties become false in the presence of +this rule? For each one that does, give a counter-example. + +$\square$ + +==== Exercise: 2 stars, optional (variation4) + +Suppose instead that we add this rule: + +```idris + ST_Funny3 : + (tpred tfalse) ->>* (tpred (tpred tfalse)) +``` + +Which of the above properties become false in the presence of +this rule? For each one that does, give a counter-example. + +$\square$ + +==== Exercise: 2 stars, optional (variation5) + +Suppose instead that we add this rule: + +```idris + T_Funny4 : + |- Tzero . TBool +``` + +Which of the above properties become false in the presence of +this rule? For each one that does, give a counter-example. + +$\square$ + +==== Exercise: 2 stars, optional (variation6) + +Suppose instead that we add this rule: + +```idris + T_Funny5 : + |- Tpred Tzero . TBool +``` + +Which of the above properties become false in the presence of +this rule? For each one that does, give a counter-example. + +$\square$ + +==== Exercise: 3 stars, optional (more_variations) + +Make up some exercises of your own along the same lines as +the ones above. Try to find ways of selectively breaking +properties -- i.e., ways of changing the definitions that +break just one of the properties and leave the others alone. + +$\square$ + +==== Exercise: 1 star (remove_predzero) + +The reduction rule `ST_PredZero` is a bit counter-intuitive: we +might feel that it makes more sense for the predecessor of zero to +be undefined, rather than being defined to be zero. Can we +achieve this simply by removing the rule from the definition of +`step`? Would doing so create any problems elsewhere? + +$\square$ + +==== Exercise: 4 stars, advanced (prog_pres_bigstep) + +Suppose our evaluation relation is defined in the big-step style. +State appropriate analogs of the progress and preservation +properties. (You do not need to prove them.) + +Can you see any limitations of either of your properties? +Do they allow for nonterminating commands? +Why might we prefer the small-step semantics for stating +preservation and progress? + +$\square$