(** Formal Type Theory, Autumn 2009, Exercise set 5 NAME(S) OF SUBMITTER(S): COMMENTS ON THE EXERCISE: Send this file (with the problems solved) to ftt09@cs.helsinki.fi by 2009-12-11 03:00+02 **) (** Once again, you can pick and mix from the exercises as you will up to a maximum of 12 points. *) Require Import tapl_ch12. Require Import tapl_ch11. (* Some symbolic names for variable identifiers. *) Definition _x := 0. Definition _y := 1. Definition _z := 2. Definition _f := 3. Definition _g := 4. (** ** Problem 1 (4 p) Study the normalization proof in Chapter 12 of TAPL and in tapl_ch12.v. Note the formulation of Lemma 12.1.5: If [x1 : T1, ..., xn : Tn |- t : T] and [v1, ..., vn] are closed values of types [T1 ... Tn] with [R_Ti(vi)] for each [i], then [R_T([x1 |-> v1] ... [xn |-> vn]t)]. An important part of the above definition is the notion that the variables of a typing context must be replaced with terms that satisfy particular constraints. In the Coq formalization, these constraints are expressed by the [env_typing] relation. It turns that the constraints are actually slightly stronger than would be really needed to carry out the proof, and we could relax them a little. This means that we could actually prove a slightly more general form of Lemma 12.1.5. Explain how the constraints can be relaxed and what changes, if any, would be needed in the proof of Lemma 12.1.5 with the relaxed requirements. - - - - - - - - - - - - - - (Answer below) - - - - - - - - - - - - - - *) Module ex2. Import typed_arith_fix. Definition well_typed t := exists T, |- t : T. (** ** Problem 2 (4 p) The normalization property doesn't hold for a language that has general recursion. Prove this by giving an explicit example of a suitable well-typed term and showing that it does not halt. Note: the example in tapl_ch11.v is not the easiest to reason with. See TAPL for an easier alternative. *) Lemma not_normalizing : exists t, well_typed t /\ ~(halts t). Proof. (** Exercise **) Admitted. (** *) End ex2. (** ** Problem 3 (4 p) Recall the computation rule for the fixed point operator: --------------------------------------------------- E-FixBeta fix (\x : T1. t2) --> [x |-> fix (\x : T1. t2)]t2 Now compare it to the function application rule: ---------------------------------- E-AppAbs (\x : T. t12) v2 --> [x |-> v2]t12 There is an obvious resemblance between these rules: on the left hand side of the evaluation arrow there is a lambda abstraction, and on the right hand side there is just the body of the abstraction, with the parameter variable substituted with something. This similarity suggests that we could streamline the language and reduce redundancy by actually considering [fix] to be a primitive function (and thus a value), and then having a special rule for applications of the [fix] function. More concretely, we would replace the production t ::= ... | fix t from the grammar and replace it by t ::= ... | fix v ::= ... | fix We would also replace the [E-FixBeta] rule with the following: ------------------- E-FixApp fix v --> v (fix v) Although this approach has a certain attraction, it is not a valid way of adding a fixpoint operator to the variants of simply typed lambda calculus that we have studied. In fact there are two separate problems that arise. Explain. - - - - - - - - - - - - - - (Answer below) - - - - - - - - - - - - - - *) Module ex4. (** ** Problem 4 In a language with pairs, there are several possible approaches to accessing the elements of pairs. One way is to have separate projection operations for the first and second element: for example, [{42, true}.1] would evaluate to [42] and [{42, true}.2] would evaluate to [true]. However, this is not the only possibility. Another option is to provide a [case] expression for accessing _both_ elements simultaneously. We are already familiar with this mechanism from Coq: in Coq, the term [match (pair 42 true) with pair x y => y end] evaluates [true]. We can add a similar construct (with a slightly different syntax) to the languages we are studying. So suppose we add to the grammar of terms the following production: t ::= case t1 of {x1, x2} => t2 The idea is that the [case] expression deconstructs the pair [t1] and binds the variables [x1] and [x2] to the first and second element of the pair, respectively, and then evaluates [t2]. This grammar fragment can be found in the file paircase_grammar.ott. consider a language with a base type, function types, and the previously encountered pair operations, as well as this new [case] construct. The Coq definitions for this language can be found in the file typed_paircase_lang.v. Note that the evaluation and typing rules have not been updated to take the new [case] expressions into account. The task is to add these. NOTE that in the problems below, the modifications to the language should preserve the determinism, progress and type preservation properties, even though you do not need to prove this formally. *) Require Import typed_paircase_lang. (** *** Problem 4.a (3 p) Add evaluation rules to the language so that the case expressions (built with the constructor [TmPairCase]) have the desired behavior. Do this formally in Coq by adding new constructors to the inductive definition of the [eval] relation below. *) Inductive eval : term -> term -> Prop := | E_App1 : forall (t1 t2 t1':term), eval t1 t1' -> eval (TmApp t1 t2) (TmApp t1' t2) | E_App2 : forall (t1 t2 t2':term), val t1 -> eval t2 t2' -> eval (TmApp t1 t2) (TmApp t1 t2') | E_AppAbs : forall (x:var) (T:type) (t12 t2:term), val t2 -> eval (TmApp (TmAbs x T t12) t2) (subst x t2 t12 ) | E_PairBeta1 : forall (t1 t2:term), val t1 -> val t2 -> eval (TmProj1 (TmPair t1 t2)) t1 | E_PairBeta2 : forall (t1 t2:term), val t1 -> val t2 -> eval (TmProj2 (TmPair t1 t2)) t2 | E_Proj1 : forall (t1 t1':term), eval t1 t1' -> eval (TmProj1 t1) (TmProj1 t1') | E_Proj2 : forall (t1 t1':term), eval t1 t1' -> eval (TmProj2 t1) (TmProj2 t1') | E_Pair1 : forall (t1 t2 t1':term), eval t1 t1' -> eval (TmPair t1 t2) (TmPair t1' t2) | E_Pair2 : forall (t1 t2 t2':term), val t1 -> eval t2 t2' -> eval (TmPair t1 t2) (TmPair t1 t2') (** Add new rules here. *) . (* Let's make sure we use the --> notation for this new eval *) Notation "t1 --> t2" := (eval t1 t2) : type_scope. (** *** Problem 4.b (1 p) Make sure that your definition has the following expected property: [t.1] evaluates in a single step to a value if and only if [case t of {x, y} => x] evaluates to the same value. If this seems impossible to prove, it may indicate that there is something wrong with your evaluation rules. Note that due to technical reasons, the Coq notation for the [TmPairCase] constructor is written with [kase]. *) Lemma ex4b : forall t v, val v -> (t.1 --> v <-> ((kase t of {_x, _y} => '_x)%tm --> v)). Proof. (** Exercise **) Admitted. (** *** Problem 4.c (3 p) Then define a typing rule for the [case] expressions by adding a new constructor to the following inductive definition. *) Inductive typing : ctx -> term -> type -> Prop := | T_Var : forall (G:ctx) (x:var) (T:type), bound x T G -> typing G (TmVar x) T | T_Abs : forall (G:ctx) (x:var) (T1:type) (t2:term) (T2:type), typing (CtxExtend G x T1) t2 T2 -> typing G (TmAbs x T1 t2) (TyArrow T1 T2) | T_App : forall (G:ctx) (t1 t2:term) (T12 T11:type), typing G t1 (TyArrow T11 T12) -> typing G t2 T11 -> typing G (TmApp t1 t2) T12 | T_Pair : forall (G:ctx) (t1 t2:term) (T1 T2:type), typing G t1 T1 -> typing G t2 T2 -> typing G (TmPair t1 t2) (TyPair T1 T2) | T_Proj1 : forall (G:ctx) (t1:term) (T1 T2:type), typing G t1 (TyPair T1 T2) -> typing G (TmProj1 t1) T1 | T_Proj2 : forall (G:ctx) (t1:term) (T2 T1:type), typing G t1 (TyPair T1 T2) -> typing G (TmProj2 t1) T2 (** Add a new rule here. *) . (* Again make sure the notations refer to the new definition. *) Notation "|- t : T" := (typing CtxEmpty t T) : type_scope. Notation "G |- t : T" := (typing G t T) : type_scope. (** *** Problem 4.d (1 p) Again, sanity-check your typing rule by showing that the following equivalence holds. *) Lemma ex4d : forall G t T, G |- t.1 : T <-> G |- (kase t of {_x,_y} => ('_x)%tm) : T. Proof. (** Exercise **) Admitted. (** **) End ex4.