A semantic framework for higher-order functional logic programming with Lambda-Abstractions

Abstract

La programación declarativa es un paradigma de programación con sólidos fundamentos matemáticos que permite diseñar programas con un alto nivel de abstracción; la programación lógico funcional aúna los formalismos lógico y funcional y ha sido un importante campo de investigación en las últimas décadas. En este trabajo se estudia un marco moderno para programación lógico funcional de orden superior con λ-abstracciones, que es una extensión de los sistemas de reescritura de patrones basada en λ-cálculo para añadir características de orden superior basadas en λ-abstracciones y unificación de orden superior a los lenguages de programación lógico funcional convencionales. En este trabajo presentamos la lógica de reescritura GHRC que tiene un cálculo asociado con el mismo nombre y que especifica formalmente la derivabilidad a partir de la lógica. Después presentamos conceptos semánticos en base a una semántica de modelos y una semántica de punto fijo. Finalmente, presentamos una extensión del marco para permitir la construcción modular de programas de orden superior y definimos una semántica modular adecuada para ello demostrando que es composicional y completamente abstracta con respecto a las operaciones definidas sobre módulos. [ABSTRACT] Declarative programming is a programming paradigm with solid mathematical foundations that allow to design programs with a very high level of abstraction; the functional logic formalism puts together functional and logic formalisms and has been an intense matter of research in the last two decades. In this work we study a modern semantic framework for higher-order functional logic programming with λ-abstractions, as an extension to pattern rewriting systems based on λ-calculus to add higher-order features based on λ-abstractions and higher-order unification to standard functional logic programming languages. We present a declarative rewriting logic GHRC with an associated calculus with the same name that formally specifies derivability from the logic. Then we present declarative semantic concepts in the form of classic model-theoretic semantics and fixed-point semantics. Finally we present an extension of the framework to support modular construction of higherorder programs and we define semantics suitable for this extension proving that they are compositional and fully abstract with respect to the classical operations defined over modules.