CSCI 6220
Solutions to practice questions for exam 2

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

    Yes, it is valid. It follows from the basic sequent a,b |- a, b by or-introduction on the right.

  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.

    The big-step semantics just says to run the small-step semantics until you get a result. I will use -> for the small-step is followed by relation, and => for the big-step relation.

    t1 -> t2, t2 => t3
    t1 => t3
    Additionally, you need an axiom stating that a value follows itself in the big-step style.

  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?

    A substitution that unifies these two is Y = a, Z = X and W = a. The result of this substitution is g(a, Z, h(a)).

  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.

    1. In functional programming the facts are equations. In logic programming they are sequents.

    2. When using facts in evaluating a functional program, you use just one of the facts for each replacement, and reach just one answer. In logic programming, you use them all, and can reach more than one answer.

  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.)

    append(A, [V|B], X), append(C, [V|D], B)

  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?

    The interpreter can defer negated goals. A setp is done in a negated goal only when it can be done without binding any variables.

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

    A refutation is a proof that a particular statement or sequent is false, by presuming that statement or sequent and deriving a contradiction. You prove that P is true by refuting not(P). In terms of sequents, not(P) is obtained by moving P to the other side of the sequent.

  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.)

    (\x.\y. x (\z.y))(\w.w 0)
    -> \y. (\w.w 0) (\z.y)
    -> \y. ((\z.y) 0)
    -> \y. y

  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.

    Remember that you can rename bound variables freely.

    succ = \x.\y.\z.y(x y z)
    c1 = \x.\y.x y
    c2 = \x.\y.x(x y)
     
    succ(c1) = (\x.\y.\z.y(x y z))(\u.\v.u v)
    -> \y.\z.y((\u.\v.u v) y z)
    -> \y.\z.y((\v.y v) z)
    -> (\y.\z.y(y z)))
    = c2