El Lenguaje CLP(H/E): Una Aproximación basada en Restricciones a la Integración de la Programación Lógica y Funcional

• Autores: María Alpuente Frasnedo
• Directores de la Tesis: Giorgio Levi (dir. tes.) , Isidro Ramos Salavert (dir. tes.)
• Lectura: En la Universitat Politècnica de València ( España ) en 1991
• Idioma: español
• Enlaces
  • Tesis en acceso abierto en: Dialnet
• Resumen
  • español

    Uno de los problemas que, en los últimos años, han atraído con más fuerza el interés de los investigadores en el campo de la Programación Lógica es el de la integración de dos de las familias más prometedoras de lenguajes declarativos: los lenguajes lógicos y los ecuacionales. Este problema ha sido afrontado con técnicas y planteamientos muy distintos. Una de las aproximaciones de mayor relevancia define un programa lógico - ecuacional (P,E) como un programa lógico positivo P (cláusulas de Horn definidas) aumentado con una teoría ecuacional de Horn E. La ventaja de esta aproximación es que, dado que la teoría ecuacional también es un conjunto de cláusulas de Horn definidas, se cumple la conocida propiedad de intersección de modelos y, así, la teoría ecuacional genera una relación de congruencia menor o más fina sobre el universo de Herbrand asociado al programa. Tomando como dominio de interpretación el cociente del universo de Herbrand módulo esta congruencia, el programa lógico extendido con la teoría ecuacional admite una semántica de modelo mínimo y una semántica por menor punto fijo. De esta forma, las principales propiedades semánticas de los programas lógicos tradicionales se preservan en un contexto más general de programación lógico - ecuacional. Concretamente, se mantiene la existencia de un dominio de computación canónico sobre el que es posible definir varias semánticas formales que no sólo son simples y elegantes sino que, además, coinciden: semántica operacional, semántica por teoría de modelos y semántica por punto fijo. Por otro lado, el paradigma de programación lógica pura ha sido generalizado recientemente a un contexto más general de programación lógica con restricciones (Constraint Logic Programming, CLP). CLP es un marco general, un esquema genérico para la introducción de restricciones en programación lógica. Cada instancia CLP(c) del esquema es un lenguaje de programación que surge especificando una estructura c de computación. El esquema CLP garantiza que las propiedades semánticas de los programas lógicos convencionales son heredadas por cualquier lenguaje que pueda formalizarse como una instancia del esquema. Además, existen modelos, correspondientes a diferentes comportamientos observables de los programas lógicos, que han sido desarrollados para el esquema y que se parametrizan también para cada una de sus instancias.

    El principal argumento discutido en esta tesis es que en el marco de CLP es posible formalizar la deseada integración entre programación lógica y ecuacional, admitiendo la definición de funciones y proporcionando un tratamiento adecuado de la relación de igualdad. La tesis define una instancia del esquema CLP especializada en resolver ecuaciones bajo una teoría ecuacional de Horn E. La estructura de computación viene dada justamente por la menor partición H/E inducida por E sobre el universo de Herbrand H para el programa. = es el único símbolo de predicado para las restricciones, interpretado como igualdad semántica en el dominio. El lenguaje propuesto, CLP(H/E), aúna el estilo de programación lógica basado en cláusulas Horn, el paradigma basado en ecuaciones (condicionales) y la programación con restricciones. La ventaja de esta nueva aproximación a la integración es que, ya que el lenguaje se define como una instancia del esquema, todas las propiedades semánticas mencionadas anteriormente son heredadas automáticamente por él. Además, si se desarrolla un procedimiento eficiente para resolver restricciones en la estructura H/E, éste puede ser incorporado fácilmente a un sistema CLP general y cooperar con otros algoritmos de resolución de restricciones.

  • English

    One of the most challenging problems in Computational Logic is the integration of two of the most popular families of declarative languages: logical languages and equational languages. A relevant approach to address this problem is based on considering an equational logic program (P, E) as a positive logic program P that is augmented by a Horn equational theory E. The advantage of this approach is that, since the equational theory E is also a set of defined Horn clauses, the program (P, E) fulfills the well-known property of model intersection, and thus generates an smallest equational congruence on the Herbrand universe associated with the program. On the interpretation domain, that is, the quotient of the Herbrand universe module this congruence, the equational logic program admits a minimal model semantics and a fixpoint semantics as well. Thus, the main semantic properties of traditional logic programs are preserved in the more general, integrated, logic-equational programming paradigm. Specifically, it maintains the existence of a canonical computation domain on which you can define several formal semantics that are not only simple and elegant but also do coincide.

    On the other hand, the pure logic programming paradigm has recently been generalized to a broader context of Constraint Logic Programming (CLP). CLP is a general framework, a generic scheme for the introduction of constraints in logic programming. Each instance CLP(C) of the scheme is a programming language that is obtained by specifying a computing structure C. The CLP scheme ensures that the semantic properties of conventional logic programs are inherited by any language that can be formalized as an instance of the schema. The main argument discussed in this thesis is that, in the context of CLP, it is possible to formalize the desired integration between logic programming and equational programming by a suitable treatment of the equality relation. The thesis defines an instance of the CLP scheme that is specialized in solving equations in an equational Horn theory E. The computer structure is given just by the smallest partition H/E induced by E on the Herbrand universe H for the program. The equality = is the only predicate symbol for constraints, that is interpreted as semantic equality in this domain. The proposed language, CLP (H/E), combines the logic programming paradigm with (conditional) equations and Constraint programming. The advantage of this new integration approach is that, since the language is defined as an instance of the CLP(C) scheme, all the semantic properties mentioned above are automatically inherited within it. Furthermore, an efficient procedure for solving constraints in the structure H/E can be easily incorporated into a general CLP system and cooperate with other constraint solving algorithms.