Khaine775
Khaine775

Reputation: 2765

Folding Set to make a new Set

Say I have a type Prop for propositions:

type Prop = 
    | P of string
    | Disjunction of Prop * Prop
    | Conjunction of Prop * Prop 
    | Negation of Prop

Where:

• A "p" representing the atom P,
• Disjunction(A "P", A "q") representing the proposition P ∨ q. 
• Conjunction(A "P", A "q") representing the proposition P ∧ q. 
• Negation(A "P") representing the proposition ¬P.

I'm supposed to use a set-based representation of formulas in disjunctive normal form. Since conjunction is commutative, associative and (a ∧ a) is equivalent to a it is convenient to represent a basic conjunct bc by its set of literals litOf(bc).

bc is defined as: A literal is an atom or the negation of an atom and a basic conjunct is a conjunction of literals

This leads me to the function for litOf:

let litOf bc = 
    Set.fold (fun acc (Con(x, y)) -> Set.add (x, y) acc) Set.empty bc

I'm pretty sure my litOf is wrong, and I get an error on the (Con(x,y)) part saying: "Incomplete pattern m atches on this expression. For example, the value 'Dis (_, _)' may indicate a cas e not covered by the pattern(s).", which I also have no clue what actually means in this context.

Any hints to how I can procede?

Upvotes: 2

Views: 101

Answers (1)

Anton Schwaighofer
Anton Schwaighofer

Reputation: 3149

I assume your example type Prop changed on the way from keyboard to here, and orginally looked like this:

type Prop = 
    | P of string
    | Dis of Prop * Prop
    | Con of Prop * Prop 
    | Neg of Prop

There are several things that tripped you up:

  • Set.fold operates on input that is a set, and does something for each element in the set. In your case, the input is a boolean clause, and the output is a set.

  • You did not fully define what constitutes a literal. For a conjunction, the set of literals is the union of the literals on the left and on the right side. But what about a disjunction? The compiler error message means exactly that.

Here's what I think you are after:

let rec literals = function
    | P s -> Set.singleton s
    | Dis (x, y) -> Set.union (literals x) (literals y)
    | Con (x, y) -> Set.union (literals x) (literals y)
    | Neg x -> literals x

With that, you will get

> literals (Dis (P "A", Neg (Con (P "B", Con (P "A", P "C")))))
val it : Set<string> = set ["A"; "B"; "C"]

Upvotes: 3

Related Questions