DOC PREVIEW
Homework

This preview shows page 1-2 out of 6 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 6 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 6 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 6 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

6.5 Exercises 131llist2A= µα. 1 ⊕ !(A ⊗ α). Here we can observe directly if the list is empty ornot, but not the head or tail which remains unevaluated.llist3A= µα. 1 ⊕ (A ⊗ !α). Here we can observe directly if the list is empty ornot, and the head of the list is non-empty. However, we cannot see thetail.llist4A= µα. 1 ⊕ (!A ⊗ α). Here the list is always eager, but the elements arelazy. This is the same as list!A.llist5A= µα. 1 ⊕ (ANα). Here we can see if the list is empty or not, but we canaccess only either the head or tail of list, but not both.infStreamA= µα. !(A ⊗ α). This is the type of infinite streams, that is, lazylists with no nil constructor.Functions such as append, map, etc. can also be written for lazy lists (seeExercise 6.15).Other types, such as trees of various kinds, are also easily represented usingsimilar ideas. However, the recursive types (even without the presence of thefixpoint operator on terms) introduce terms which have no normal form. In thepure, untyped λ-calculus, the classical examples of a term with no normal formis (λx. x x)(λx. x x)whichβ-reduces to itself in one step. In the our typedλ-calculus (linear or intuitionistic) this cannot be assigned a type, because x isused as an argument to itself. However, with recursive types (and the fold andunfold constructors) we can give a type to a version of this term which β-reducesto itself in two steps.Ω=µα. α → αω :Ω→Ω=λx:Ω. (unfold x) xThenω (foldΩω)−→β(unfold (foldΩω)) (foldΩω)−→βω (foldΩω).At teach step we applied the only possible β-reduction and therefore the termcan have no normal form. An attempt to evaluate this term will also fail,resulting in an infinite regression (see Exercise 6.16).6.5 ExercisesExercise 6.1 Prove that if Γ; ∆ ` M : A and Γ; ∆ ` M : A0then A = A0.Draft of November 8, 2001132 Linear λ-CalculusExercise 6.2 A function in a functional programming language is called strictif it is guaranteed to use its argument. Strictness is an important concept in theimplementation of lazy functional languages, since a strict function can evaluateits argument eagerly, avoiding the overhead of postponing its evaluation andlater memoizing its result.In this exercise we design a λ-calculus suitable as the core of a functionallanguage which makes strictness explicit at the level of types. Your calculusshould contain an unrestricted function type A → B, a strict function typeA  B, a vacuous function type A 99K B, a full complement of operatorsrefining product and disjoint sum types as for the linear λ-calculus, and a modaloperator to internalize the notion of closed term as in the linear λ-calculus. Yourcalculus should not contain quantifiers.1. Show the introduction and elimination rules for all types, including theirproof terms.2. Given the reduction and expansions on the proof terms.3. State (without proof) the valid substitution principles.4. If possible, give a translation from types and terms in the strict λ-calculusto types and terms in the linear λ-calculus such that a strict term is well-typed if and only if its linear translation is well-typed (in an appropriatelytranslated context).5. Either sketch the correctness proof for your translation in each directionby giving the generalization (if necessary) and a few representative cases,or give an informal argument why such a translation is not possible.Exercise 6.3 Give an example which shows that the substitution [M/w]Nmust be capture-avoiding in order to be meaningful. Variable capture is a sit-uation where a bound variable w0in N occurs free in M,andwoccurs in thescope of w0. A similar definition applies to unrestricted variables.Exercise 6.4 Give a counterexample to the conjecture that if M −→βM0andΓ; ∆ ` M0: A then Γ; ∆ ` M : A. Also, either prove or find a counterexampleto the claim that if M −→ηM0and Γ; ∆ ` M0: A then Γ; ∆ ` M : A.Exercise 6.5 The proof term assignment for sequent calculus identifies manydistinct derivations, mapping them to the same natural deduction proof terms.Design an alternative system of proof terms from which the sequent derivationcan be reconstructed uniquely (up to weakening of unrestricted hypotheses andabsorption of linear hypotheses in the >Rrule).1. Write out the term assignment rules for all propositional connectives.2. Give a calculus of reductions which corresponds to the initial and principalreductions in the proof of admissibility of cut.3. Show the reduction rule for the dereliction cut.Draft of November 8, 20016.5 Exercises 1334. Show the reduction rules for the left and right commutative cuts.5. Sketch the proof of the subject reduction properties for your reductionrules, giving a few critical cases.6. Write a translation judgment S =⇒ M from faithful sequent calculusterms to natural deduction terms.7. Sketch the proof of type preservation for your translation, showing a fewcritical cases.Exercise 6.6 Supply the missing rules for ⊕E in the definition of the judg-ment Γ; ∆I\ ∆O`iM : A and show the corresponding cases in the proof ofLemma 6.4.Exercise 6.7 In this exercise we explore the syntactic expansion of extendedcase expressions of the form case M of m.1. Define a judgment which checks if an extended case expression is valid.This is likely to require some auxiliary judgments. You must verify thatthe cases are exhaustive, circumscribe the legal patterns, and check thatthe overall expression is linearly well-typed.2. Define a judgment which relates an extended case expression to its expan-sion in terms of the primitive let, case,andabort constructs in the linearλ-calculus.3. Prove that an extended case expression which is valid according to yourcriteria can be expanded to a well-typed linear λ-term.4. Define an operational semantics directly on extended case expressions.5. Prove that your direct operational semantics is correct on valid patternswith respect to the translational semantics from questions 2.Exercise 6.8 Define the judgment M −→∗βM0via inference rules. The rulesshould directly express that it is the congruent, reflexive and transitive closureof the β-reduction judgment M −→βM0. Then prove the generalized subjectreduction theorem 6.6 for your judgment. You do not need to show all cases,but you should carefully state your induction hypothesis in sufficient generalityand give a few critical parts of the proof.Exercise 6.9 Define weak β-reduction


Homework

Download Homework
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view Homework and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Homework 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?