Assignment 1:Grammars and Induction15-312: Foundations of Programming LanguagesMatt Moore ([email protected])Out: Thursday, September 2, 2004Due: Thursday, September 9, 2004 (1:30 pm)50 points totalWelcome to 15-312! This assignment focuses on context-free grammarsand inductive proofs. It is due September 9that the start of lecture. You areencouraged, but not required, to typeset your answers; if you write themout by hand, write legibly. If I can’t read it, I can’t give credit for it.Please make sure you understand the policy on collaboration; refer tohttp://www.cs.cmu.edu/˜fp/courses/312/assignments.html1 Grammars (35 points)Consider the grammar G over the alphabet Σ = {int, list, -> , ( , ) }with nonterminals tycon and type:tycon ::= int | tycon list | ( type)type ::= tycon | type -> typeQuestion 1.1 (5 points).The first production for tycon can be written in rule notation asint tyconWrite grammar G in rule notation.1Grammar G is flawed: it does not pin down the associativity of ->. Forexample, there are two different derivations of the string int->int->int.We can fix the ambiguity by changing the second production of type fromtype ::= type -> typetotype ::= tycon -> typeMaking this change results in the grammar G0below. To avoid confu-sion, we rename tycon to tycon0and type to type0.tycon0::= int | tycon0list | ( type0)type0::= tycon0| tycon0-> type0Question 1.2 (5 points).Write grammar G0in rule notation.Note, however, that we have not shown that this new grammar G0isequivalent to G, that is, that the languages of type and type0are the same:L(type) = L(type0). This can be proved in two steps: first prove L(type0) ⊆L(type), then prove L(type) ⊆ L(type0).Question 1.3 (10 points).Prove L(type0) ⊆ L(type) by provingIf s type0then s typeby induction. If you need to generalize the induction hypothe-sis, be sure to clearly state your generalized induction hypoth-esis. If you need any lemmas, state them explicitly and provethem.Question 1.4 (15 points).Prove L(type) ⊆ L(type0) by provingIf s type then s type0As in the previous question, clearly state any generalized in-duction hypothesis and prove any lemmas you need.22 Propositional logic (15 points)In this question we will look at a subset of Propositional Logic. Our universeof terms consists of an infinite number of nullary operators P0, P1, . . . , Pn(“propositional variables”) and the binary operator ⇒ (“implication”). Wedefine the sets prop and thm over this universe:PipropVarA prop B prop(A ⇒ (B ⇒ A)) thmKA prop B prop(A ⇒ B) propImpA prop B prop C prop((A ⇒ (B ⇒ C)) ⇒ ((A ⇒ B) ⇒ (A ⇒ C))) thmS(A ⇒ B) thm A thmB thmAppTruth Value. If we have assignments (to true or false) for all of the propo-sitional variables in a proposition, its truth value (either true or false)can be computed recursively using the following familiar truth table for ⇒:Proposition Truth Value(false ⇒ false) true(false ⇒ true) true(true ⇒ false) false(true ⇒ true) trueTautology. A proposition is a tautology iff for every assignment of truthvalues (true, false) to the propositional variables P0, . . . , Pn, the truthvalue of the proposition is true.Question 2.1 (15 points).Prove, using rule induction, that if A thm then A is a tautology.Question 2.2 (EXTRA CREDIT).Find a proposition A that is a tautology, but not a theorem (thatis, the judgment A thm cannot be derived). You do not need toprove that it is not a