| Assigned: | Tuesday, September 29 |
| Due: | Wednesday, October 14, 11:59pm |
You can call your program file whatever you want, but parsesequent.cmg assumes that it is called sequent.cmg. If you want to use a different name, change the import line in parsesequent.cmg.
You will need to copy parsesequent.cmg into the same directory as your program file.
I assume that you are familiar with the basics of propositional logic. We will restrict ourselves to a subset that allows propositional variables and operations ¬, ∧, ∨ and ⇒. (See the precedence rules.)
We say that a propositional formula is valid if it is true no matter what values the propositional variables have. For example, P ∨ ¬P is a valid propositional formula, as is P∧Q ⇒ P∨Q.
Sequent logic is described in the textbook in exercise 5.17, pages 219 and 220. A sequent has the form α |– β where α and β are lists of formulas. Sequent α |– β means "If all of the formulas in list α are true then at least one of the formulas in list β is true."
For example, sequent P, Q |– P, Q says that, if P and Q are both true then at least one of P and Q is true.
If the left-hand list in a sequent is empty, it is treated as true. So sequent |‐ P ⇒ P says that formula P ⇒ P is true.
If the right-hand list in a sequent is empty, it is treated as false, So P∧¬P |– says that, if P∧¬P is true then false is true. Since false is not true, that sequent can be read as saying that P∧¬P is false.
A sequent is valid if it is true no matter what the values of the variables are. All of the sequents shown in this section are valid.
We will use notation for sequents where a formula or English letter refers to just a single formula while a Greek letter refers to a list of formulas. For example, x, α |‐ β indicates that the left-hand list consists of formula x followed by the formulas in list α.
A sequent is basic if some formula occurs in both the left-hand list and the right-hand list. For example, sequent P, Q |– P, Q is basic, as is P, Q |– Q.
Every basic sequent is valid. That gives us a starting point for proving that other, nonbasic sequents are valid.
A rule of inference lets you derive new valid sequents from other sequents that you already know are valid. Page 220 of the textbook shows some rules of inference. Each shows one or more sequents above a line and one sequent below the line. Such a rule means that, if you know that all of the sequents above the line are valid, then the sequent below the line is valid.
There are two rules for each logical operator; one rule adds a formula with the given operator to the left-hand list and one rule adds a formula with the given operator to the right-hand list.
A goal-directed proof works backwards. You start with a sequent that you want to prove valid. Find an inference rule that would work. (That is discussed below.) Then prove each of the sequents that is above the line in the rule. Each of those proofs also proceeds in a goal-directed fashion.
Eventually, you wind up trying to prove one of two kinds of sequents. In one case, the sequent is basic, and you can conclude that it is valid.
In the other case, the sequent is not basic, but all of its formulas are just propositional variables; there are no logical operators. A nonbasic sequent with no logical operators is always invalid. For example, sequent P |– Q is not valid.
The assignment is to write a Cinnameg program that reads a sequent and responds by saying whether the sequent is valid. You are required to do this using the design below.
Try to use higher order functions to make the program shorter and simpler.
For this assignment you will need to write types. A value of type Formula is a propositional formula. A value of type Sequent is a sequent. (Formula and Sequent are defined in the template file.)
If f is a function that takes a parameter of type A and yields a result of type β, then f has type A → β. (The arrow is written in programs as ->.)
Ordered pair (true, "goat") has type (Boolean, String).
If x is a list whose members have type T, then x has type [T].
Maybe of Integer is a type whose members have two kinds: nothing and something(n), where n is an integer. Value nothing indicates that there is nothing here. Value something(n) indicates integer n; so there is something here. (You can think of nothing as analogous to null in Java.)
You will want to use type Maybe of [Sequent] as the result type of a function that handles an inference rule. The function returns something(L) if L is a list of subgoals that come out of the inference rule. It returns nothing if the inference rule cannot be applied at all.
You will want to provide an expectation for each of your functions. Paragraph
Expect isInferable: Formula -> Boolean.indicates that you will define a function called isInferable that takes a formula as a parameter and yields a boolean result.
If you write an expectation for a function then you can use that function anywhere in the program (before or after the expectation and the definition.)
It is a good idea to say what a function does. Here is an example of that.
Expect isInferable: Formula -> Boolean
%: isInferable(x) is true if formula x is
%: not just a propositional variable.
%Expect
Get the template file. Use it as a starting point. It defines types Formula and Sequent.
There are five kinds of formula: A variable (with a name), and one for each logical operator. Expression vbl "P" \/ vbl "Q" is the formula P ∨ Q.
There is just one kind of sequent. Expression [vbl "P", vbl "Q"] |- [vbl "Q"] is sequent P, Q |– Q.
You can use type constructors in patterns. For example, case
case f(vbl name) = …is only used if the parameter is a formula that is a variable, and
case f(a /\ b) = …is only used if the formula is a conjunction. Similarly,
g(alpha |- beta) = …says that g takes a sequent as its parameter, with left-hand list alpha and right-hand list beta.
Define a function that tests whether a given sequent is basic. Use someSatisfy and `in`.
Define a function for each rule of inference that has type Sequent &rightarrow Maybe of [Sequent]. (You can also call that type Rule, using the abbreviation given in the template file.) It should take a goal sequent (underneath the line in the inference rule) and yield either nothing (if the inference rule does not apply to the given sequent) or something(L) where L is a list of the sequents above the line in the inference rule.
Assume that the formula of interest is at the beginning of the list of formulas. Do not search the list. For example, rule negL can be defined by
case negL (neg x :: alpha |- beta) = something [alpha |- x :: beta] case negL (?) = nothingsince, if you have already proved that sequent α |– x, β is valid, then you can conclude that sequent x, &alpha |– β is also valid.
A formula is inferable if it contains a logical operator. Write a function that takes a formula and returns true if it is inferable. Also write a function that takes a list of formulas and returns true if it contains at least one inferable formula. Use someSatisfy.
Define a function that takes a list of formulas and returns a reordered version of the list that begins with an inferable formula. If there is no inferable formula in the list, it should return the list unchanged. Use select and operator −/.
Write a function that takes a list of sequents and returns true if every sequent in the list is valid. Use allSatisfy. (You will need to use a function that tests whether a single sequent is valid, which you have not yet written. I hope that doesn't bother you.)
Write a function that takes a sequent and a list of Rules (that is, a list of functions), and tries to use each rule on the sequent. If a rule applies, it should use that rule to get one or two new goals, and should test whether the new goals are valid.
If a rule can be used and the new goals are valid, this function should return true. (That is, it has found a proof that the sequent is valid.) If none of the rules applies, or if it is not possible to prove one of the new goals, this function should return false, indicating that it has not found a validity proof using the given list of rules.
Write functions inferLeft and inferRight, where inferLeft tries all of the left-rules (not-left, etc.) and inferRight tries all of the right-rules.
Make inferLeft and inferRight return true if successful.
Write function infer, which moves an inferable sequent to the front of the left-hand list, if possible, uses inferLeft if that is possible. If the left-hand list does not contain an inferable formula, it should try a similar thing on the right-hand list.
Make infer return true if successful.
Write a function that takes a sequent and tells whether the sequent is valid. Test for a basic sequent. For a non-basic sequence, see if an inference rule helps.
Write valid?, which takes a formula and returns true if it is valid. Formula x is valid if and only if sequent |– x is valid. (That is, make the left-hand list empty and the right-hand list hold just x.)
Write a separate tester. You can make it read
a sequent or read lines of text and convert each
line to a sequent. Import parsesequent.cmg
for a parser that converts a string into a sequent or formula. You can use
Match $(s: Sequent) = str.
to convert a string to a sequent called s, and
Match $(f: Formula) = str.
to convert str to a formula called f.
If you want to read just one formula or sequent from
the standard input, the following will work.
Extract $(s: Sequent).
Extract $(f: Formula).
Write formulas as you would in a program,
except that a variable is just a name consisting
of one or more letters and that you use &minus for
negation. Write a sequent by writing
a comma-separated list of zero or more formulas, then |-,
then another comma-separated list of zero or more formulas.
You can put spaces between things (or not) and you can
use parentheses. For example,
P \/ Q, -Q |- (P /\ Q ==> P \/ Q), P
is a sequent.
If you write a formula as a string in a program, be sure to double all backslashes. For example, "P \\/ Q" is P \/ Q.
The syntax is as follows.
sequent → formulas |- formulas
formulas → formula , formulas
| formula
formula → sum ==> formula
| sum
sum → term \/ sum
| term
term → component /\ term
| component
component → - component
| ( formula )
| vblname
vblname → letter
| letter vblname
Instead of providing only a yes or no answer concerning the validity of a sequent or formula, rework the program so that it yields a proof. Be sure to keep a copy of the version that does not include the extra credit so that you have a backup in case this does not work out.
First, add the following to the export part of your package.
============================================= %% Inference ============================================= %: inference(old, new) indicates that new is %: inferred based on prior inferences in %: list old. ============================================= Type Inference = inference ([Sequent], Sequent). ============================================= %% Proof ============================================= %: A proof is either nothing, indicating %: that the proof was not successful, or is %: a list of inferences that prove a given %: sequent. ============================================= Abbrev Proof = Maybe of [Inference].
Also add the following to the expectations.
proof: Sequent -> Proof
%: proof(s) yields one of the following.
%: If s is valid:
%: something(lst) where lst is a list of
%: inference steps used to prove s.
%:
%: If s is not valid:
%: nothing
;
ShowProof: Proof -> ();
cmg.$: Inference -> String;
In the implementation part, write definitions of proof and ShowProof. Here is a definition of $ for Inference. Symbol |= is used in mathematical logic to mean "proves." It is like the horizontal line in a rule of inference, but for cases where you write the rule in one line.
============================================================== %% $ (Inference) ============================================================== Define $(inference(a,b)) = $(a) ++ " |= " ++ $(b).
You will want to make some functions that yield boolean results in the original program yield values of type Proof instead. You will probably find the following useful.
Abbrev
MaybeSeqList = Maybe of [Sequent];
Rule = Sequent -> MaybeSeqList
%Abbrev
Be sure to plan your ideas before you start coding.
The validity problem is the problem of determining whether a given propositional formula is valid. In general, the validity problem takes a long time to solve. It belongs to a family of problems called CoNP-complete problems, and all of those problems are conjectured not to have any algorithm that runs in time nk for any fixed k, where n is the length of the formula.
It is possible that you will run into that issue when asking whether particular formulas are valid; your program will run a long time. You can reduce the time by giving preference to inference rules that only have one sequent above the line, so that you reduce the proliferation of subgoals. But you are not required to do that.
¬
∧
∨
⇒
By convention, ¬ has the highest precedence, followed by ∧, then ∨, with ⇒ having the lowest precedence.