CSCI 6220
Practice questions for exam 2

  1. Is a,b |- a \/ b a valid propositional sequent? (|-<\tt> is turnstile and \/ is the "or" operator.)

  2. Given a small-step semantics that defines relation ->, you can define a big-step semantics that defines the down-arrow relation. The inference rules for down-arrow can use premises about relation ->. Describe such a big-step semantics, in general.

  3. For this question, lower case letters stand for functions and constants, and upper case letters stand for variables. Give a substitution unifies term g(a,X,h(Y)) with g(Y, Z, h(W)) in the most general possible way, and what term results from performing that substitution?

  4. Functional programming and logic programming are both kinds of declarative programming, where a program is a collection of facts. List two significant differences in their points of view, in terms of what kinds of facts programs state, how computation is performed, how you reason about programs, what kinds of tasks programs are suitable for, what kinds of results programs give, etc. Do not get sidetracked by syntactic issues.

  5. The append predicate is defined so that append(X,Y,Z) is true if list Z is equal to list X followed by list Y. For example, append([a,b,c],[d,e],[a,b,c,d,e]) is true. Without defining any new predicates, write a goal that is true just when list X contains some value more than once. (You are not looking for a specific value, but want to know whether there exists a value v that occurs in X more than once.)

  6. Logic programming typically uses Horn sequents rather than general sequent for its axioms. That presents a problem when you want to use negation. Negation-as-failure can be used to provide negation in a logic-programming interpreter. What additional feature of an interpreter is required to make negation-as-failure logically sound?

  7. What is a refutation? How can a refutation be used to prove a positive fact?

  8. This question uses \ for lambda. If you reduce term (\x.\y. x (\z.y))(\w.w 0) until there are no more redexes, what do you get? (Term 0 stands for the Church numeral c0.)

  9. Using the definitions of Church numerals c1, c2 and succ given in class, show that term (succ c1) can be transformed into c2 by performing reductions of redexes.