F#: is it OK for developing theorem provers?

Question

Please advise. I am a lawyer, I work in the field of Law Informatics. I have been a programmer for a long time (Basic, RPG, Fortran, Pascal, Cobol, VB.NET, C#). I am currently interested in F#, but I'd like some advise. My concern is F# seems to be fit for math applications. And what I want would require a lot of Boolean Math operations and Natural Language Processing of text and, if successful, speech. I am worried about the text processing.

I received a revolutionary PROLOG source code (revolutionary in the field of Law and in particular Dispute Resolution). The program solves disputes by evaluating Yes-No (true-false) arguments advanced by two debating parties. Now, I am learning PROLOG so I can take the program to another level: evaluate the strenght of arguments when they are neither a Yes or No, but a persuasive element in the argumentation process.

So, the program handles the dialectics aspect of argumentation, I want it to begin processing the rhetoric aspect of argumentation, or at least some aspects.

Currently the program can manage formal logic. What I want is to begin managing some aspects of informal logic and for that I would need to do parsing of strings (long strings, maybe ms word documents) for the detection of text markers, words like "but" "therefore" "however" "since" etc, etc, just a long list of words I have to look up in any speech (verbal or written) and mark, and then evaluate left side and right side of the mark. Depending on the mark the sides are deemed strong or weak.

Initially, I thought of porting the Prolog program to C# and use a Prolog library. Then, it ocurred to me maybe it could be better in pure F#.

Answer 1

First, the project you describe sounds (and I believe this is the correct legal term) totally freaking awesome.

Second, while F# is a good choice for math applications, its also extremely well-suited for any applications which perform a lot of symbolic processing. Its worth noting that F# is part of the ML family of languages which were originally designed for the specific purpose of developing theorem provers. It sounds like you're writing an application which appeals directly to the niche ML languages are geared for.

I would personally recommend writing any theorem proving applications you have in F# rather than C# -- only because the resulting F# code will be about 1/10th the size of the C# equivalent. I posted this sample demonstrating how to evaluate propositional logic in C# and F#, you can see the difference for yourself.

Answer 2

F# has many features that make this type of logic processing natural. To get a feel for what the language looks like, here is one possible way to decide which side of an argument has won, and by how much. Uses a random result for the argument, since the interesting (read "very hard to impossible") part will be parsing out the argument text and deciding how persuasive it would be to an actual human.

/// Declare a 'weight' unit-of-measure, so the compiler can do static typechecking
[<Measure>] type weight

/// Type of tokenized argument
type Argument = string

/// Type of argument reduced to side & weight
type ArgumentResult =
    | Pro of float<weight>
    | Con of float<weight>
    | Draw

/// Convert a tokenized argument into a side & weight
/// Presently returns a random side and weight
let ParseArgument =
    let rnd = System.Random()
    let nextArg() = rnd.NextDouble() * 1.0<weight>
    fun (line:string) ->
        // The REALLY interesting code goes here!
        match rnd.Next(0,3) with
        | 1 -> Pro(nextArg())
        | 2 -> Con(nextArg())
        | _ -> Draw

/// Tally the argument scored
let Score args = 
    // Sum up all pro & con scores, and keep track of count for avg calculation
    let totalPro, totalCon, count =
        args
        |> Seq.map ParseArgument
        |> Seq.fold
            (fun (pros, cons, count) arg ->
                match arg with
                | Pro(w) -> (pros+w, cons, count+1)
                | Con(w) -> (pros, cons+w, count+1)
                | Draw   -> (pros, cons,   count+1)
                )
             (0.0<weight>, 0.0<weight>, 0)
    let fcount = float(count)
    let avgPro, avgCon = totalPro/fcount, totalCon/ fcoun
    let diff = avgPro - avgCon
    match diff with
    // consider < 1% a draw
    | d when abs d < 0.01<weight>   -> Draw
    | d when d > 0.0<weight>        -> Pro(d)
    | d                             -> Con(-d)

let testScore = ["yes"; "no"; "yes"; "no"; "no"; "YES!"; "YES!"]
                |> Score
printfn "Test score = %A" testScore