F#: ¿está bien para el desarrollo de los probadores de teoremas?
(6)
F # no admite la programación lógica como Prolog. es posible que desee revisar el compilador de P # .
Por favor avise. Soy abogada, trabajo en el campo de Informática del Derecho. He sido programador durante mucho tiempo (Básico, RPG, Fortran, Pascal, Cobol, VB.NET, C #). Actualmente estoy interesado en F #, pero me gustaría un consejo. Mi preocupación es que F # parece ser adecuado para aplicaciones matemáticas. Y lo que quiero requiere una gran cantidad de operaciones matemáticas booleanas y procesamiento del lenguaje natural del texto y, si tiene éxito, habla. Estoy preocupado por el procesamiento de texto.
Recibí un código fuente revolucionario de PROLOG (revolucionario en el campo del derecho y, en particular, de la resolución de disputas). El programa resuelve las controversias evaluando los argumentos de Sí-No (verdadero-falso) presentados por dos partes en el debate. Ahora, estoy aprendiendo PROLOG para poder llevar el programa a otro nivel: evaluar la fuerza de los argumentos cuando no son un Sí o un No, sino un elemento persuasivo en el proceso de argumentación.
Entonces, el programa maneja el aspecto dialéctico de la argumentación, quiero que comience a procesar el aspecto retórico de la argumentación, o al menos algunos aspectos.
Actualmente el programa puede gestionar la lógica formal. Lo que quiero es comenzar a administrar algunos aspectos de la lógica informal y para eso tendría que hacer un análisis de las cadenas (cadenas largas, tal vez más documentos de Word) para la detección de marcadores de texto, palabras como "pero" "por lo tanto" "sin embargo" "Desde", etc., etc., solo una larga lista de palabras que tengo que buscar en cualquier discurso (verbal o escrito) y marcar, y luego evaluar el lado izquierdo y el lado derecho de la marca. Dependiendo de la marca, los lados se consideran fuertes o débiles.
Inicialmente, pensé en portar el programa Prolog a C # y usar una biblioteca Prolog. Entonces, me ocurrió que tal vez podría ser mejor en F # puro.
F # tiene muchas características que hacen que este tipo de procesamiento lógico sea natural. Para tener una idea de cómo se ve el lenguaje, aquí hay una manera posible de decidir qué lado de una discusión ha ganado y por cuánto. Utiliza un resultado aleatorio para el argumento, ya que la parte interesante (leída "muy difícil a imposible") analizará el texto del argumento y decidirá qué tan persuasivo sería para un humano real.
/// 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
Parece que los aspectos funcionales de F # son atractivos para usted, pero se pregunta si puede manejar los aspectos no funcionales. Debe saber que F # tiene todo el .NET Framework a su disposición. Tampoco es un lenguaje puramente funcional; Puede escribir código imperativo en él si lo desea.
Finalmente, si aún hay cosas que desea hacer desde C #, es posible llamar funciones F # desde C #, y viceversa.
Portar de prólogo a F # no será tan sencillo. Si bien ambos son lenguajes no imperativos. Prolog es un lenguaje declarativo y f # es funcional. Nunca utilicé las bibliotecas de C # Prolog, pero creo que será más fácil que luego convertir todo a f #.
Primero, el proyecto que usted describe suena (y creo que este es el término legal correcto) totalmente increíble.
En segundo lugar, si bien F # es una buena opción para aplicaciones matemáticas, también es extremadamente adecuado para cualquier aplicación que realice una gran cantidad de procesamiento simbólico. Vale la pena señalar que F # es parte de la familia de lenguajes ML que se diseñaron originalmente con el propósito específico de desarrollar probadores de teoremas. Parece que estás escribiendo una aplicación que apela directamente a los lenguajes de nicho ML diseñados para.
Personalmente recomendaría escribir cualquier aplicación de prueba de teoremas que tengas en F # en lugar de C #, solo porque el código F # resultante será aproximadamente 1/10 del tamaño del equivalente de C #. Publiqué este ejemplo que demuestra cómo evaluar la lógica proposicional en C # y F #, puedes ver la diferencia por ti mismo.
Si bien F # es ciertamente más adecuado que C # para este tipo de aplicaciones, ya que habrá varios algoritmos que F # le permite expresar de una manera muy concisa y elegante, debe considerar la diferencia entre programación funcional, OO y lógica. De hecho, portar desde F # probablemente requerirá que uses un solucionador (o implementes el tuyo) y eso te puede llevar algo de tiempo acostumbrarte. De lo contrario, debería considerar crear una biblioteca con su código de prólogo y acceder a él desde .NET (vea más sobre interoperabilidad en esta página y recuerde que a todo lo que puede acceder desde C # también puede acceder desde F #).