F #: это нормально для разработки доказательств теорем?

Question

Пожалуйста, сообщите. Я юрист, работаю в области юридической информатики. Я был программистом в течение длительного времени (Basic, RPG, Fortran, Pascal, Cobol, VB.NET, C #). В настоящее время я заинтересован в F #, но я хотел бы получить совет. Меня беспокоит, что F # подходит для математических приложений. И то, что я хочу, потребовало бы большого количества операций с булевой математикой и обработки текста на естественном языке и, в случае успеха, речи. Я беспокоюсь об обработке текста.

Я получил революционный исходный код PROLOG (революционный в области права и, в частности, разрешения споров). Программа разрешает споры, оценивая аргументы Да-Нет (истина-ложь), выдвинутые двумя участниками дискуссии. Сейчас я изучаю PROLOG, чтобы я мог вывести программу на другой уровень: оценить силу аргументов, когда они не являются ни «да», ни «нет», а являются убедительным элементом в процессе аргументации.

Итак, программа обрабатывает диалектический аспект аргументации, я хочу, чтобы она начала обрабатывать риторический аспект аргументации или, по крайней мере, некоторые аспекты.

В настоящее время программа может управлять формальной логикой. Я хочу начать управлять некоторыми аспектами неформальной логики, и для этого мне понадобится выполнить синтаксический анализ строк (длинные строки, возможно, документы MS Word) для обнаружения текстовых маркеров, таких слов, как «но», «следовательно», «однако». «с тех пор» и т. д., просто длинный список слов, которые я должен найти в любой речи (устной или письменной) и отметить, а затем оценить левую и правую стороны знака. В зависимости от знака стороны считаются сильными или слабыми.

Сначала я подумал о переносе программы Prolog на C # и использовании библиотеки Prolog. Затем мне показалось, что может быть лучше в чистом F #.

Answer 1

Во-первых, проект, который вы описываете, звучит (и я считаю, что это правильный юридический термин), совершенно офигенный.

Во-вторых, хотя F # является хорошим выбором для математических приложений, он также чрезвычайно хорошо подходит для любых приложений, которые выполняют много символьной обработки. Стоит отметить, что F # является частью семейства языков ML, которые изначально были разработаны для конкретной цели разработки средств доказательства теорем. Похоже, вы пишете приложение, которое обращается непосредственно к нишевым языкам ML.

Я бы лично порекомендовал написать любые приложения для доказательства теорем на F #, а не на C # - только потому, что полученный код F # будет примерно на 1/10 размера эквивалента C #. Я разместил этот образец , демонстрирующий, как оценивать пропозициональную логику в C # и F #, вы можете увидеть разницу сами.

Answer 2

F # имеет много функций, которые делают этот тип логической обработки естественным. Чтобы понять, как выглядит язык, вот один из возможных способов определить, какая сторона аргумента выиграла и на сколько. Использует случайный результат для аргумента, поскольку интересная часть (читай «очень трудно или невозможно») будет анализировать текст аргумента и решать, насколько убедительным он будет для реального человека.

/// 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

Answer 3

Портирование от пролога до F # не будет таким простым. Хотя оба они не являются императивными языками. Пролог является декларативным языком, а f # функционален. Я никогда не использовал библиотеки C # Prolog, но думаю, что будет проще, чем конвертировать все в f #.

Answer 4

Звучит так, будто вам нравятся функциональные аспекты F #, но вам интересно, справится ли он с нефункциональными аспектами. Вы должны знать, что F # имеет в своем распоряжении весь .NET Framework. Это также не чисто функциональный язык; Вы можете написать императивный код в нем, если хотите.

Наконец, если вы все еще хотите что-то сделать из C #, можно вызывать функции F # из C # и наоборот.

Answer 5

F # не поддерживает логическое программирование, как Пролог. Возможно, вы захотите проверить P # компилятор .

Answer 6

Хотя F #, безусловно, более подходит, чем C #, для такого рода приложений, поскольку будет несколько алгоритмов, которые F # позволяет вам выразить очень кратким и элегантным способом, вам следует учитывать разницу между функционалом, ОО и логическое программирование. На самом деле, портирование с F #, скорее всего, потребует от вас использования решателя (или реализации вашего собственного), и это может занять некоторое время, чтобы привыкнуть. В противном случае вам следует подумать о создании библиотеки с вашим кодом пролога и получить к ней доступ из .NET (подробнее о взаимодействии см. на этой странице и помните, что все, к чему вы можете обращаться из C #, вы также можете получить из F #).