Assignment #1:Judgements, Induction, and the Simply Typed Lambda CalculusNathan Harmata, Michael Sullivan, for 15-312: Principles of Programming LanguagesOut: Monday, January 24Due:Theory: Tuesday, February 1 1:30pmImplementation: Thursday, February 3 11:59pm1 Introduction1.1 Course InformationAs a reminder, the website for the course ishttp://www.andrew.cmu.edu/course/15-312-sp11/If you have questions, please email the course staff or post them to the course bboard:[email protected] SubmissionSolutions to the theory questions should be handed in in class on Thursday, January 27.Submit solutions to the programming problems by 11:59 PM, Thursday, February 3 by placing your*.sml files in your hand-in directory/afs/andrew.cmu.edu/course/15/312-sp11/handin/<yourandrewid>/assn1/You are not required to typeset the written portion of the assignment, but it is highly encouraged . If youchoose to do so, refer to the appendix for details. If you instead choose to handwrite your solutions, pleasetry to be as legible as possible. Turn in your solutions at the beginning of class on the due date.2 Theory2.1 Structural Properties of DerivabilityIn this assignment you may use structural properties of derivability (reflexivity, weakening, exchange, con-traction, transitivity) without proof. Refer to your class notes and/or Ch 2.1 of PFPL for more details.12.2 InversionInference rules provide a mechanism for forward reasoning. If you can derive the premises, then you canderive the conclusion. If there is only one possible rule that could have been used to derive a judgement,then you may assume the premises of that rule. These properties are stated as Inversion Lemmas.For example, given the definition of natural numbers0 nat0-natn natS(n) natS-natwe can prove the following inversion lemma: Suppose that n nat. If n = S(n′) then n′nat.Inversion lemmas are typically proven by inspection.In this assignment you may use any inversion lemmas without proof, but you must clearly state saidinversion lemmas before using them.2.3 The Simply Typed Lambda CalclulusParts of this assignment make use of the Simply Typed Lambda Calculus, which is summarized in theappendix. The presentation of the STLC used on this homework is mostly the same as the presentation fromlecture, with the addition of the b term. The b term is the sole closed value of type o. This differs from thepresentation from lecture in which there were no closed terms of type o.2.4 Alpha-EquivalenceRecall that two terms are alpha-equivalent if they are identical except for the names of bound variables.Throughout this class, we will view the world through “alpha-equivalence goggles.” That is, we will treatas identical alpha-equivalent terms and we will freely alpha-vary terms (that is, change the names of boundvariables) when it is convenient.Task 2.1 (4%). State whether the following pairs of STLC terms are alpha-equivalent to each other#Term #1 Term #2 Alpha-Equivalent?(1) (λx:o.x) b b(2) λx:o.y x λy:o.y x(3) λx:o.y x λy:o.z x(4) λx:o → o.λy:o.x y λx:o.λy: o → o.y x(5) λx:o → o.λy:o.x y λz:o → o.λw :o.z w2.5 Rules RuleTask 2.2 (6%). Give derivations of the following judgements about the simply-typed lambda calculus. Referto the rules presented in the appendix.1. ((λx:o → o.x) (λy:o.y)) b : o2. (λx:o.λy:o → o.y x) b 7→ λz:o → o.z b22.6 Silly JudgementsIn this section, we will explore admissibility (|=) & derivability (⊢).Recall that for derivability, J ⊢RJ′is defined as “J′is derivable from the rules R∪J”. Foradmissibility,J |=RJ′is defined as “If J is derivable from the rules R, then J′is derivable from the rules R”.We define the syntactic class S of sequences of playing card suits with the following grammar:S ::= ♥| ♠| ♦| ♣| (S, S)Consider the following set of rules R1concerning the judgements S , and S .♥ ,(1)A ,(A, B) ,(2)♠ (3)A  B (A, B) (4)Task 2.3 (9%). Prove or disprove the following1. (♥, ♠)  |=R1♥ 2. (♠, ♦) , |=R1♠ ,3. ♦  ⊢R1(♦, ♠) Now consider the following set of rules R2♦ ,(5)B ,(A, B) ,(6)♥ (7)Task 2.4 (9%). Do your answers to the previous task change (under the new rule set R1∪ R2)? Explain.1. (♥, ♠)  |=R1∪R2♥ 2. (♠, ♦) , |=R1∪R2♠ ,3. ♦  ⊢R1∪R2(♦, ♠) 2.7 Induction, Induction, Induction2.7.1 SubstitutionCapture-avoiding substitution is one of the fundamental building blocks we use in defining programminglanguages. Thus, it is important to know that substitution is well-behaved. The important property thatsubstitution must have is that it is type-preserving. Specifically, we want to show thatTheoremIf Γ, x : τ2⊢ e1: τ1and Γ ⊢ e2: τ2then Γ ⊢ [e2/x]e1: τ13You may recall that this theorem was an important part of proving the Preservation Theorem of ourlanguage. Without it holding, our language wouldn’t be type-safe!Task 2.5 (2%). This theorem should be proven using induction. But on what? State what you will beinducting on, and give your inductive statement.Task 2.6 (20%). Prove the above substitution theorem.11In practice, we are only concerned with the this theorem instantiated with the empty context, however it is necessary to provethe stronger statement about any context (as you will hopefully realize when developing your proof). For theorems we encounterlater on in the course, this technique of proving a stronger result may be useful.43 Implementation3.1 OverviewFor this assignment, you will be implementing a typechecker and an evaluator for the Simply Typed LambdaCalculus, as well as some other useful functions on STLC terms. The typechecker and evaluator will beimplemented using de Bruijn indexes to represent variables. Because explicit variable naming is typicallyeasier for humans to work with, tests will be written in with explicit variables and you will also be requiredto write functions to translate between named form and De Bruijn form. Refer to the appendix for rulesgoverning the static and dynamic semantics of the STLC. These will be helpful when implementing thecomponents of this assignment.3.2 Overview of the supplied codeBefore you begin, you should read through the provided code (especially the signatures) to gain an under-standing of the setup. All of the necessary SML files are listed in sources.cm, and you can build theproject in SML/NJ by typing CM.make ‘‘sources.cm’’. The following files are