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

Ответ 1

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

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

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

Ответ 2

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

Ответ 3

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

Ответ 4

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

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

Ответ 5

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

Ответ 6

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