CODEWITHSUNDEEP
functional-programminglogicsmlml
Cheikh Ahmadou
Cheikh Ahmadou

Reputation: 59

Propositional Logic Valuation in SML

I'm trying to define a propositional logic valuation using SML structure. A valuation in propositional logic maps named variables (i.e., strings) to Boolean values.

Here is my signature:

signature VALUATION =
sig
    type T
    val empty: T
    val set: T -> string -> bool -> T
    val value_of: T -> string -> bool
    val variables:  T -> string list
    val print: T -> unit
end;

Then I defined a matching structure:

structure Valuation :> VALUATION =
        struct
            type T = (string * bool) list
            val empty = []
            fun set  C a b = (a, b) :: C
            fun value_of [] x = false
                | value_of ((a,b)::d) x = if x = a then b else value_of d x  
            fun variables [] = []
                | variables ((a,b)::d) =  a::(variables d ) 
            fun print valuation = 
                (
                    List.app
                        (fn name => TextIO.print (name ^ " = " ^ Bool.toString (value_of valuation name) ^ "\n"))
                        (variables valuation);
                    TextIO.print "\n"
                )
        end;

So the valuations should look like [("s",true), ("c", false), ("a", false)]

But I can't declare like a structure valuation or make an instruction like: [("s",true)]: Valuation.T; When I tried to use the valuation in a function, I get errors like:

Can't unify (string * bool) list (*In Basis*) with
      Valuation.T

Could someone help me? Thanks.

Upvotes: 1

Views: 276

Answers (1)

molbdnilo
molbdnilo

Reputation: 66371

The type Valuation.T is opaque (hidden).
All you know about it is that it's called "T".
You can't do anything with it except through the VALUATION signature, and that signature makes no mention of lists.

You can only build Valuations using the constructors empty and set, and you must start with empty.

- val e = Valuation.empty;
val e = - : Valuation.T
- val v = Valuation.set e "x" true;
val v = - : Valuation.T
- val v2 = Valuation.set v "y" false;
val v2 = - : Valuation.T
- Valuation.value_of v2 "x";
val it = true : bool
- Valuation.variables v2;
val it = ["y","x"] : string list
- Valuation.print v2;
y = false
x = true

val it = () : unit

Note that every Valuation.T value is printed as "-" since the internal representation isn't exposed.

Upvotes: 1

Related Questions