Popular in Course
verified elite notetaker
Popular in Computer Information Technology
verified elite notetaker
This 11 page Class Notes was uploaded by Kathleen Cartwright on Monday September 28, 2015. The Class Notes belongs to CIS500 at University of Pennsylvania taught by B.Pierce in Fall. Since its upload, it has received 9 views. For similar materials see /class/215372/cis500-university-of-pennsylvania in Computer Information Technology at University of Pennsylvania.
Reviews for SOFTWAREFOUNDATIONS
Report this Material
What is Karma?
Karma is the currency of StudySoup.
You can buy or earn more Karma at anytime and redeem it for class notes, study guides, flashcards, and more!
Date Created: 09/28/15
C18 500 i Software Foundations Midterm I Review questions with answers October 10 2007 Work each of the review problems yourself before looking at the answers given here If your answer differs from ours7 make sure you understand why P E0 Functional Programming Consider the following Fixpo int de nition in Coql Fixpoint fold XSet YSet f XgtYgtY 11ist X bY struct 1 match 1 with Inilgtb Ihtgtfhfoldftb end What is the type of fold lie7 What does Check fold print Answer fold forall X Y Set X gt Y gt Y gt list X gt Y gt Y What does Check fold plus print Answer fold nat nat plus list nat gt nat gt nat What does Eval simpl in fold plus onetwothreefour one print Answer eleven nat Recall that the map function takes a function f of type XgtY and a list 1 With elements of X and returns a list With elements of type Y containing the result of applying f to each element of 1 Which of the following Fixpoint de nitions correctly implements the map function Circle the correct answer a Fixpoint m1 XSet YSet fXgtY 11ist X struct 1 match 1 with I nil gt nil Y I h t gt h list Y 2 m1 X Y f t end b Fixpoint m2 XSet YSet fXgtY 11ist X struct 1 list Y match 1 with I nil gt f nil Y I h t gt f h m2 X Y f t end c Fixpoint m3 XSet YSet fXgtY 11ist X struct 1 list Y match 1 with I nil gt nil Y I h t gt f h m3 X Y f t end d Fixpoint m4 XSet YSet fXgtY 11ist X struct 1 list Y matchlwithInilgtni1YIhtgtfhfm4Xth end e Fixpoint m5 XSet YSet fXgtY 11ist X struct 1 list Y matchlwithInilgtnilYIhtgtfhftend f None of the above Answer 0 5 The every function takes a predicate p a oneargument function returning a yesno and a list 1 it returns yes if p returns yes on every element of 1 and no otherwise Lemma checkfi1ter1 every nat even twofourzero yes Proof simp1 reflexivity Qed Lemma checkfi1ter2 every nat even twoonefourzero no Proof simp1 reflexivity Qed What is the type of every Answer forall X Set X gt yesno gt list X gt yesno 6 Complete the following de nition of every as a recursive function Fixpoint every XSet pXgtyesno 11ist X struct 1 yesno match 1 with I ni1 gt I h t gt bothyes end Answer Fixpoint every XSet pXgtyesno 11ist X struct 1 yesno match 1 with I ni1 gt yes I h t gt bothyes p h every p t end 7 Complete the following de nition of every by supplying appropriate arguments to fold Definition every XSet pXgtyesno 11ist X yesno fold fun x acc gt bothyes Answer Definition every XSet pXgtyesno 11ist X yesno fold fun x acc gt bothyes p x ace 1 yes Coq Basics Brie y explain the difference between the tactics apply and rewritel Are there situations Where either 9 one can be applied Answer The rewrite tactic is used to apply a known equality to either the goal or a hypothesis in the context replacing all occurrences of one side by the other The apply tactic uses a known implication a hypothesis from the context a previously proved lemma or a constructor to modify the proof state either backward the goal matches the conclusion of the implication in which case a subgoal is generated for each premise of the implication or forward some hypothesis matches the premise of the implication in which case this hypothesis is replaced by the conclusion of the implication If the fact is itself an equality e an implication with no premises then either tactic can be use Brie y explain the difference between the tactics destruct and induction Answer Both are used to perform case analysis on an element of an inductively de ned type induction also generates an induction hypothesis while destruct does not 50 10 The following proof attempt is not going to succeed Brie y explain Why and how it can be xed Lemma doub1einjective forall m n double m double n gt m n Proof intros m n induction m Case quot0quot simpl intros eq destruct n Case quot0quot reflexivity Case quotSquot inversion eq Case quotSquot intros eq destruct n Case quot0quot inversion eq Case quotSquot assert m n as H Case quotProof of assertionquot Answer Because the induction hypothesis is insu iciently general 7 it gives us a fact involving one particular n but to nish the last step of the proof we need to know something about a di erent n To x it either use generalize dependent n before induction or else just omit intros m n Inductively De ned Sets 11 Suppose we give Coq the following declarations Inductive mumble Set I a mumble I b mumble gt nat gt mumble I c mumble Inductive grumble XSet Set I d mumble gt grumble X I e X gt grumble X Which of the following are welltyped members of the set grumble a d b a five Answer No b d mumble b a five Answer Yes c d yesno b a five Answer Yes d e yesno yes Answer Yes e e mumble b c zero Answer Yes f e yesno b c zero Answer No g c Answer No H E0 Consider the following inductive de nition Inductive baz Set I x baz gt baz I y baz gt yesno gt baz How many elements does the set baz have Answer None 13 Consider the following inductive de nition Inductive tree Set I leaf tree I node tree gt tree gt tree Describe7 in English7 the elements of the set treei Answer Unlabeled binary trees 14 What induction principle Will Coq generate for tree Answer treeind forall P tree gt Prop leaf gt forall t tree gt forall t0 tree P to gt P node 1 110 gt forall t tree P 1 Alternate answer the one above is What Coq actually generates7 but it is logically equivalent to this arguably more natural variant treeind forall P tree gt Prop P leaf gt forall t1 t2 tree P 131 gt P 132 gt P node 131 112 gt forall t tree P t 15 Here is an induction principle for an inductively de ned set 5 mysetind forall P myset gt Pro forall y yesno P conl y gt forall n nat m myset P m gt P con2 n m gt forall m myset P In What is the de nition of myset Answer Inductive myset Set I conl yesno gt myset I con2 nat gt myset gt myset 16 Consider the following inductive de nition nat gt Set Inductive stree I leaf stree one forall m n stree m gt stree n gt stree plus m n I node Describe7 in English7 the elements of the set stree seveni Answer Unlabeled binary trees with exactly seven leaves In general for each n the set stree it contains binary trees with n total leaves Inductively De ned Propositions 17 Consider the following inductively de ned family of propositions Inductive p tree gt nat gt Prop 2 I c1 p leaf one I c2 forall t1 t2 n1 n2 p t1 n1 gt p t2 n2 gt p node t1 t2 plus n1 n2 Describe7 in English7 the conditions under Which the proposition p t n is provablel Answer This proposition is provable when t is an unlabeled binary tree with exactly n leaves That is p is a relation between trees and numbers that relates each tree to its number of leaves 18 Consider the following inductively de ned family of propositions Inductive bar nat gt Prop I d bar six I e forall 11 bar times n n I f bar three gt bar five For Which n is the proposition bar n provable Answer bar n is provable when n is either six or a perfect square zero one four nine etc Programming With Propositions 19 The concept of composition of relations can be de ned as follows Suppose Q and R are both relations on a set X The composition of Q and R is the relation C such that7 for all x and z in X7 sz lt gt HlexyARyzl Write an Inductive de nition in Coq that expresses this concept Answer Inductive composition X Set Q R relation X X gt X gt Prop comp forall x 2 exists y Q x y R y z gt composition X Q R x z 20 Give the de nition of logical conjunction and as an inductive proposition in Coql Answer Inductive and A B Prop Prop 2 conj A gt B gt and A B Operational Semantics 21 Recall the de nition of the set tm7 the predidate value7 and the relation eval from the lecture notes Inductive tm Set I tmconst nat gt tm I tmplus tm gt tm gt tm Inductive value tm gt Prop 2 vconst forall n value tmconst n Inductive eval tm gt tm gt Prop I EPlusConstConst forall n1 n2 eval tmplus tmconst n1 tmconst n2 tmconst plus n1 n2 I EPlus1 forall t1 t1 t2 eval t1 t1 gt eval tmplus t1 t2 tmplus t1 t2 I EPlus2 forall v1 t2 t2 value v1 gt eval t2 t2 gt eval tmplus v1 t2 tmplus v1 t2 Which of the following propositions are provable a eval tmplus tmconst one tmconst two tmconst plus one two Answer Yes b eval tmplus tmplus tmconst one tmconst two tmconst three tmconst plus plus one two three Answer No c eval tmplus tmplus tmconst one tmconst two tmplus tmconst three tmconst four tmplus tmplus tmconst one tmconst two tmconst plus three four Answer No Recall the determinism and progress theorems for the eval relation Theorem eva1deterministic partia1function eval Theorem eva1progress forall t value 1 exists t eval t t a Suppose we add a new constructor to the evaluation relation as follows N N I EFunny1 eval tmconst zero tmconst zero ii Does eva1deterministic continue to hold Answer No iii Does eva1progress continue to hold Answer Yes b Suppose we remove the constructor vconst from the de nition of value ii Does eva1deterministic continue to hold Answer Yes iii Does eva1progress continue to hold Answer No c Is there any way we can cause eva1progress to fail by adding new constructors to the de nition of eval Answer No
Are you sure you want to buy this material for
You're already Subscribed!
Looks like you've already subscribed to StudySoup, you won't need to purchase another subscription to get this material. To access this material simply click 'View Full Document'