CS254 ASSIGNMENTS, Week 1, Due Feb 12, 1999 Readings: pp 1-67 Background + PCF Syntax SIGN UP IN ORDER FROM TOP TO BOTTOM Sign up for just one thing. (There are many things listed this time because of uncertainty of class size.) You need to bring one Xeroxable written solution of each exercise you sign up for. An instructor will give class presentations not signed up for, or at the second course meeting will give class presentations of exercises a student has signed up for if the student wishes (the student must still supply a written solution). Class Presentations: Be Sure to include new examples. ____________________ PCF Syntax (p 65) ____________________ PCF Syntactic Extensions (p 66) ____________________ Ex 2.2.7 Deriving Rules ____________________ Ex 2.2.6 Substitution Identities Darko_Marinov_______ Ex 2.2.8 Uncurry ____________________ Ex 1.7.3 Parsing ____________________ Ex 2.2.12 Two Argument Functions Exercises: Latex Writeups are Encouraged. ____________________ 2.2.15 Mutual Recursion Jessica_Fong________ 2.2.13 Static/Dynamic Scope (2 person; ____________________ or one person just a&b&c) Jason_Carroll_______ 2.2.3 Exponentiation Requires Recursion (Hint: see 1.8.6) ____________________ 2.2.16 Letrec as Basic (2 person) (or one person just a&b) ____________________ ____________________ 1.8.15 Well Founded Sets ____________________ 1.8.11 Structural Induction ____________________ 1.3.2 Reduction Mini-Explosion ____________________ 1.6.6 Function Properties ____________________ 1.8.5 Integer Induction Hard Exercises: No deadline. ____________________ 1.3.3 Reduction Explosion CS254 ASSIGNMENTS, Week 2, Due Feb 19, 1999 Readings: pp 67-132 PCF This is an unusually difficult one week reading. To lighten the load, we suggest skimming or skipping: 2.5.4 and 2.5.4 Connection to Recursive Function Theory 2.5.6 Nondefinability of Parallel Operations Also note that any material dealing with denotational semantics may be hard to understand here, but is covered much more carefully later in the book. To lighten the load we moved Lifted Types into the following week's reading, and furthermore plan to suggest next week that much of Lifted Types be skipped. Given that, next week's reading should be easier and may allow a bit of catchup from this week. The heart of this weeks reading are the 4 operational semantics and the sum and recursive type extensions. Class Presentations: Be Sure to include new examples. ____________________ Axiomatic Semantics (Table 2.1) Darko_Marinov_______ Operational Semantics (Table 2.2) ____________________ Leftmost Reduction (Table 2.3) ____________________ Lazy Reduction (Table 2.4) ____________________ Eager Reduction (Table 2.5) ____________________ Ex 2.4.24 Reason for Eager Delay ____________________ Unit and Sum Types ____________________ Recursive Types ____________________ 2.6.7 Typing the Untyped Lambda Calculus Exercises: Latex Writeups are Encouraged. Jessica_Fong________ 2.6.3 Proofs for Sum Types Nate_Kushman________ 2.6.4 Sum Extensionality Inconsistency ____________________ 2.5.27 Dependency on Subexpression Termination ____________________ 2.6.8 Transcribing ML Types ____________________ 2.4.25 Eager Delay and Y [ \z.Ux for x should read \z.Uz for z] ____________________ 2.6.6 The List Recursive Type ____________________ 2.3.3 Recursive Proof Rule [Hint: compute fix from itself] ____________________ 2.4.9 Recursive Non-Confluence Example ____________________ 2.4.18 Expression with No Normal Form ____________________ 2.3.5 Independence of =op from Set of Observable Types ____________________ 2.5.11 Tail Recursive GCD CS254 ASSIGNMENTS, Week 3, Due Feb 26, 1999 Readings: pp 132-203 Lifted Types, Universal Algebra This should be easier reading than last week. We still suggest skimming or skipping: pp 140-144 Translation of Eager PCF into PCF_|_ The heart of this week's reading is term algebras, quotient algebras, and initial algebras. Class Presentations: Be Sure to include new examples. ____________________ Translation of PCF to PCF_|_ ____________________ Algebras and Interpretations ____________________ Soundness and Completeness ____________________ Term, Quotient, and Initial Algebras ____________________ 3.5.6 and 3.5.7 Properties of Homomophisms Darko_Marinov_______ 3.6.3 Multiset Algebras ____________________ 3.6.6 Final Multiset Algebra ____________________ Error Values Exercises: Latex Writeups are Encouraged. ____________________ 3.6.7 Error Handling Nate_Kushman________ 3.5.16 Natural Number Algebras Jessica_Fong________ 3.4.19 Derived Substitution Rule ____________________ 2.6.13 Pointed Types CS254 ASSIGNMENTS, Week 4, Due Mar 5, 1999 Readings: pp 203-257 Rewrite Systems, Simply Typed Lambda Calculus This weeks read is a bit shorter than next week's, so if you have time to get a head start on next week's, do so. Class Presentations: Be Sure to include new examples. ____________________ Rewrite Systems, Confluence, Provable Equality Darko_Marinov_______ Termination Darko_Marinov_______ 3.7.20 Termination ____________________ Critical Pairs and Confluence ____________________ Left Linear Non-Overlapping Rewrite Systems ____________________ 3.7.36 Knuth-Bendix Algorithm ____________________ Type Inferences and the Typing Algorithm Exercises: Latex Writeups are Encouraged. Jessica_Fong________ 3.6.7 and 3.7.37 Error Elements ____________________ 4.3.12 Induction on Typing Derivations ____________________ 4.3.16 Intuitionistic Logic Nate_Kushman________ 4.3.18 Computation of Types CS254 ASSIGNMENTS, Week 5, Due Mar 12, 1999 Readings: pp 257-317 Simply Typed Lambda Calculus Proof Systems and Henkin Models, Intro to CPOs This reading is shortened a bit when compared to the syllabus, because this reading is not easy. Class Presentations: Be Sure to include examples. ____________________ Rules and Axioms for Equations of the Simply Typed Lambda Calculus ____________________ Reduction Rules for the Simply Typed Lambda Calculus, Confluence and Strong Normalization ____________________ Consistency and Conservativity Darko_Marinov_______ Henkin Models Darko_Marinov_______ 4.5.19 Extending Algebras to Henkin Models ____________________ Soundness and Completeness ____________________ Combinators ____________________ Intro to CPOs Exercises: Latex Writeups are Encouraged. Nate_Kushman________ 4.4.12, 4.5.21, 4.5.26 Untyped Lambda Calculus ____________________ 4.5.36 Type Frames for Extended Simply Typed Lambda Calculus ____________________ 4.5.35 Combinator Substitution ____________________ 4.5.24 and 4.5.29 Empty Types Jessica_Fong________ 5.2.18 CPO Proofs Hard Exercises: No deadline. ____________________ 4.5.12 Equality between Functionals ____________________ 4.4.15, 4.5.20, 4.5.27 Higher-Order Logic CS254 ASSIGNMENTS, Week 6, Due Mar 19, 1999 Readings: pp 318-386 CPOs, Fixed Point Induction, Computational Adequacy, Full Abstraction, Modest Sets, PERs This reading is hard taken all together. Suggest you skip or skim PERs (5.6) and if necessary modest sets (5.5). Class Presentations: Be Sure to include examples. ____________________ Fixed Points in CPOs and Full Continuous Hierarchy ____________________ CPO Model for PCF ____________________ Fixed Point Induction ____________________ Computational Adequacy ____________________ Full Abstraction Note: modest sets and PERs will not be covered in class Exercises: Latex Writeups are Encouraged. ____________________ 5.4.19 Full Abstraction of pairs ____________________ 5.4.15, 5.4.16, and 5.4.18, Compactness and BLUB Jessica_Fong________ 5.3.3 Fixed Point Induction ____________________ 5.2.42 PCF + tree model ____________________ 5.2.33 Sums in the Full Continuous Hierarchy Hard Exercises: No deadline. ____________________ 5.4.9 Fix Inference Soundness ____________________ 5.3.5 Pairwise Recursion CS254 ASSIGNMENTS, Week 7, Due Mar 25, 1999 Note WE WILL MEET Thur 11am-1pm, Mar 25, ESL 412. The different meeting time is for this week only. Readings: pp 387-444 Imperative Programs This reading is a bit easier than some weeks. Class Presentations: Be Sure to include examples. ____________________ Syntax of While Programs Ex 6.2.3 ____________________ Operational Semantics ____________________ Denotational Semantics Ex 6.4.4 ____________________ Partial Correction Assertion Syntax ____________________ Partial Correction Assertion Proof Rules and Soundness ____________________ Relative Completeness Note: Additional Program Constructs will not be covered in class but you should read the material. Exercises: Latex Writeups are Encouraged. ____________________ 6.5.1 Partial Correctness using Denotational Semantics [Please work out the denotational semantics of each program fragment explicitly.] Darko_Marinov_______ 6.5.7 Partial Correctness using Proof Rules ____________________ 6.6.12 Recursive Procedure Denotational Semantics ____________________ 6.6.7 A New Proof Rule [side conditions of rule are not quite right] ____________________ 6.6.8 Use of Fixed Point Induction ____________________ 6.5.11 Expressiveness Failure ____________________ 6.5.12 Decidability Result ____________________ 6.3.3 and 6.3.4 One Step Operational Semantics CS254 ASSIGNMENTS, Week 8, Due Apr 8, 1999 Note WE WILL NOT MEET next week (ending Apr 2). This is Harvard Spring Vacation. If you have not yet finished at least 5 exercises or presentations please use the vacation to catch up. Note WE WILL MEET Thur 11am-1pm, Apr 8, ESL 412. The different meeting time is for this week only. Readings: pp 445-505 Cartesian Closed Categories This reading is hard because you need to do more of the exercises in order to understand the material. Suggest you skip or skim 7.3. Chapter 7 as a whole may be skipped or skimmed as the author promises it will not be used later. Note that a main idea of cartesian closed categories for beginners is to establish 7.2.19 as a model of the simply typed lambda calculus. It fails to be a Henkin model because it is not extensional. Class Presentations: Be Sure to include examples. ____________________ Categories. Example 7.2.16 ____________________ Products, Exponentials, Terminals, and CCC's. Example 7.2.19, Exercise 7.2.24 ____________________ Term Interpretation and Soundness. ____________________ The Meaning Function as a Functor. Note: Kripke Lambda Models and Functor Categories will not be covered in class. Exercises: Latex Writeups are Encouraged. ____________________ 7.2.39 Completeness of the Term Category. [You may shorten the proof by giving only harder cases.] ____________________ 7.2.49 Meaning is a Functor ____________________ 7.2.23 Henkin Model Categories are CCC. ____________________ 7.2.38 Meaning in Henkin Categories. [You may shorten the proof by giving only harder cases.] CS254 ASSIGNMENTS, Week 9, Due Apr 16, 1999 Readings: pp 505-573 Recursive Type Domain Models, Logical Relations You should read Chapter 8, pp 535-573, about Logical Relations, FIRST, and then read 7.4.1 to get the idea of what Recursive Type Domains are about. Read the rest of Chapter 7 only if you have the time and desire. We will NOT talk about recursive type domains in class. Class Presentations: Be Sure to include examples. ____________________ Logical Relations. Darko_Marinov_______ Basic Lemma. Darko_Marinov_______ Acceptable Meaning and Admissible Relations. ____________________ Logical Partial Equivalence Relations. ____________________ Quotient Models. ____________________ Completeness. ____________________ Type-Closed Properties. Exercises: Latex Writeups are Encouraged. ____________________ 8.2.29 and 8.2.28 Beta implies admissiblility and substitution. [Do 8.2.29 first.] ____________________ 8.3.3 Completeness with Empty Types ____________________ 8.3.13 Eta Postponement. CS254 ASSIGNMENTS, Week 10, Due Apr 23, 1999 Readings: pp 573-638 More Logical Relations, Polymorphism You should read Chapter 9, pp 607-638, about Polymorphism, FIRST; then re-read last week's assignment about Logical Relations to be sure you understand it, and then if you have time read the rest of Chapter 8. We will talk about Polymorphism in class, and if we have time, review some more of last weeks reading on Logical Relations. Class Presentations: Be Sure to include examples. ____________________ Predicative Syntax with Types. ____________________ Impredicative and Type:Type. ____________________ Equational Proof and Reduction. ____________________ Henkin Models. ____________________ Polymorphic Let. Exercises: Latex Writeups are Encouraged. ____________________ 9.2.5 Subtype Relaxation. ____________________ 9.2.8 Substitution in Derivations. ____________________ 9.2.12 Strong Normalization. CS254 ASSIGNMENTS, Week 11, Due Apr 30, 1999 Readings: pp 639-701 Impredicative Polymorphism, Data Abstraction You should read Section 9.4 about Data Abstraction FIRST; then read the beginning of 9.3 about Impredicative Polymorphism, at least up through the Church Numerals ending on p 644. Then re-read last week's assignment about Predicative Polymorphism to be sure you understand it, and then if you have time read the rest of Section 9.3. We will talk about Data Abstraction in class, and a little bit about Impredicative Polymorphism. Class Presentations: Be Sure to include examples. ____________________ Data Abstraction. ____________________ Predicative Products and Sums. ____________________ Impredicative Polymorphism. ____________________ Church Numerals. Exercises: Latex Writeups are Encouraged. ____________________ 9.5.7 Type Equality Rules ____________________ 9.4.4 Complex Numbers ____________________ 9.3.4 Weak Products CS254 ASSIGNMENTS, Week 12, Due May 7, 1999 Readings: pp 703-763 Subtyping Read pp 703-727 first and then 10.5 and 10.6. If you have time read the pages skipped on subset and PER interpretations. Class Presentations: Be Sure to include examples. ____________________ Subtyping Axioms and Rules. ____________________ Records. ____________________ Conversion Interpretation. ____________________ Recursive Record Types. ____________________ Subtype Polymorphism and Inheritance. Exercises: Latex Writeups are Encouraged. ____________________ 10.2.8 and 10.3.5 Minimum Types ____________________ 10.2.9 and 10.3.6 Subject Reduction ____________________ 10.4.12 Derivation Canonical Form ____________________ 10.5.7 Infinite Expansion Equality [Some of these are hard] CS254 ASSIGNMENTS, Week 13, Due May 14, 1999 Readings: pp 765-815 Type Inference Read this from beginning to end. 11.3.4 and 11.3.5 at the end are less important than the rest of the chapter. Class Presentations: Be Sure to include examples. ____________________ Simply Typed Lambda Calculus with Type Variables. ____________________ Principal Curry Typings. ____________________ ML Typing Rules. ____________________ ML Type Inference. Exercises: Latex Writeups are Encouraged. ____________________ 11.2.7 Graph Unification ____________________ 11.2.8 Unification Algorithm ____________________ 11.2.9 Unification Algorithm Lemma ____________________ 11.2.14 Principal Typing Algorithm CS254 ASSIGNMENTS, Week 14, Due May 21, 1999 There is no additional reading or additional exercises. You must turn in all work to Bob Walton, ESL 408, by 5pm May 21, either as hardcopy or email. The final course requirement is 10 exercises, some of which may be replaced by class presentations of parts of the text book or of other topics approved by the instructor.