CS 451/LLC Lab 4: Working with terms and folds

Due Monday 6 March 2006

  1. Abstract interpretation

    Write an abstract interpreter for arithmetic expressions over integer literals (including zero and negative values), at least one variable (you might use a constructor Var), and the binary operators Add, Mul and Sub (interpreted as addition, multiplication and subtraction).

    (See the Wikipedia article onabstract interpretation for some motivations and metaphorical examples. Note especially that the results you get will generally be inexact, i.e., you may generate "unknown" even if a better approximation is actually discernible.)

    Your interpreter should compute the "polarity" of an expression (its sign, more or less). The space of possible polarity values should be the enumerated type:

    data Polarity = Unk | Neg | Zero | Pos
    where the values are interpreted as unknown, negative, zero and positive, respectively. Make sure to use the fold function for terms to do the work: you'll need only give it semantic interpretations for the operators (and literals and variables) which are appropriate to the abstract value domain (in other words, literals and variables will be classified in terms of their apparent polarity and operators will be of type Polarity -> Polarity -> Polarity Hint: write out tables for the operators before you do anything else: in other words, for what combinations of polarity inputs do the operators return which polarity results?

  2. Interpreter for simple propositional logic

    Define a type for terms of a simple propositional logic with boolean literals, operators for conjunction (AND), disjunction (OR) and implication (IF-THEN), plus two propositional variables (you can think of them as P and Q if you like).

    You might use the expression type from above as a basis for your work, but you'll need to make some changes, unless you generalize the definition to allow for different types of literals, variables and operators by via suitable type parameterization. You may use an enumerated type or Strings or Chars as "carriers" for the variable and operator symbol types (but I recommend the enumerated approach).

    You may need to modify the definition of fold to account for your a new term structure, unless you use the generalized type approach.

    You can then use fold to define the semantics of Boolean terms as functions on pairs of values (representing the values of the variables P and Q). So your meaning function will look like this:

    val :: BExpr -> (Bool,Bool) -> Bool
    val t (p,q) = fold ...

  3. Tautology checker for simple propositional logic

    Using the above implementation of valuation for propositional terms, write a function which will tell whether a given term is a tautology, i.e., whether it always has the value True, for all possible assignments of values to the variables P and Q. Think in terms of a truth table: generate the list of all possible pairs of Booleans first, then use either map or all to combine your evaluation function with this list of possibilities (all takes a prediacte and a list and tells whether the predicate is true of everything in the list).