type-systems - relacion - razonamiento en lenguaje formal

¿Qué tipo de sistemas pueden evitar la suspensión de goles en lenguajes lógicos?

Question

De la sección 3.13.3 del tutorial de curry :

Las operaciones que residen se llaman rígidas, mientras que las operaciones que restringen se llaman flexibles. Todas las operaciones definidas son flexibles, mientras que la mayoría de las operaciones primitivas, como las operaciones aritméticas, son rígidas, ya que adivinar no es una opción razonable para ellas. Por ejemplo, el preludio define una operación de concatenación de listas de la siguiente manera:

infixr 5 ++
...
(++)             :: [a] -> [a] -> [a]
[]       ++ ys   = ys
(x:xs) ++ ys     = x : xs ++ ys

Dado que la operación "++" es flexible, podemos usarla para buscar una lista que satisfaga una propiedad en particular:

Prelude> x ++ [3,4] =:= [1,2,3,4]       where x free
Free variables in goal: x
Result: success
Bindings:
x=[1,2] ?

Por otro lado, las operaciones aritméticas predefinidas como la adición "+" son rígidas. Por lo tanto, una llamada a "+" con una variable lógica como un argumento falla:

Prelude> x + 2 =:= 4 where x free
Free variables in goal: x
*** Goal suspended!

Curry no parece protegerse contra los objetivos de escritura que serán suspendidos. ¿Qué tipo de sistemas pueden detectar con anticipación si un objetivo se va a suspender?

Answer 1

Lo que ha descrito suena como una verificación de modo, que generalmente verifica qué salidas estarán disponibles para un determinado conjunto de entradas. Es posible que desee comprobar el idioma de Mercury, que toma la comprobación de modo bastante en serio.