Person: Rodríguez Hortalá, Juan
Universidad Complutense de Madrid
Faculty / Institute
Lenguajes y Sistemas Informáticos
Now showing 1 - 7 of 7
PublicationRewriting and call-time choice(2008-05-12) Rodríguez Hortalá, JuanNon-confluent and non-terminating rewrite systems are interesting from the point of view of programming. In particular, existing functional logic languages use such kind of rewrite systems to define possibly non-strict non-deterministic functions. The semantics adopted for non-determinism is call-time choice, whose combination with non-strictness is not a trivial issue that has been addressed from a semantic point of view in the Constructor-based Rewriting Logic (CRWL) framework. In a recent serie of works we have investigated how to express call-time choice and non-strict semantics from a point of view closer to classical rewriting. We propose a notion of rewriting which uses an explicit representation for sharing with let-constructions and is proved to be equivalent to the CRWL approach. During this talk we will address the following issues: - We will briefly review some of the main existing approaches for describing the semantics of functional logic languages: CRWL, traditional rewriting and Curry’s à la Launchbury operational semantics. - We will present the let-rewriting relation for first order functional logic programs, and its semantic equivalence with CRWL logic. - We will discuss the relation between all these semantic approaches, and present some technicall results concerning this relations. - We will see some interesting properties of the combined framework CRWL/letrewriting, and show by a case study (correctness of bubbling) the usefulness of the achieved combination of semantic and reduction notions. - We will extend our let-rewriting relation providing a notion of let-narrowing which is adequate for call-time choice as proved by soundness and completeness results of let-narrowing with respect to let-rewriting. Completeness is based on a lifting lemma for let-rewriting similar to Hullot’s lifting lemma for ordinary rewriting and narrowing. 1 PublicationSafe typing of functional logic programs with opaque patterns and local bindings(Elsevier, 2014-04) López Fraguas, Francisco J.; Martín Martín, Enrique; Rodríguez Hortalá, JuanType systems are widely used in programming languages as a powerful tool providing safety to programs. Functional logic languages have inherited Damas-Milner type system from their functional part due to its simplicity and popularity. In this paper we address a couple of aspects that can be subject of improvement. One is related to a problematic feature of functional logic languages not taken under consideration by standard systems: it is known that the use of opaque HO patterns in left-hand sides of program rules may produce undesirable effects from the point of view of types. We re-examine the problem, and propose two variants of a Damas-Milner-like type system where certain uses of HO patterns (even opaque) are permitted while preserving type safety. The considered formal framework is that of programs without extra variables and using let-rewriting as reduction mechanism. The other aspect addressed is the different ways in which polymorphism of local definitions can be handled. At the same time that we formalize the type system, we have made the effort of technically clarifying the overall process of type inference in a whole program. PublicationNew Results on Type Systems for Functional Logic Programming(Springer, 2010) López Fraguas, Francisco; Martín Martín, Enrique; Rodríguez Hortalá, JuanType systems are widely used in programming languages as a powerful tool providing safety to programs, and forcing the programmers to write code in a clearer way. Functional logic languages have inherited Damas & Milner type system from their functional part due to its simplicity and popularity. In this paper we address a couple of aspects that can be subject of improvement. One is related to a problematic feature of functional logic languages not taken under consideration by standard systems: it is known that the use of opaque HO patterns in left-hand sides of program rules may produce undesirable effects from the point of view of types. We re-examine the problem, and propose a Damas & Milner-like type system where certain uses of HO patterns (even opaque) are permitted while preserving type safety, as proved by a subject reduction result that uses HO-let-rewriting, a recently proposed reduction mechanism for HO functional logic programs. The other aspect is the different ways in which polymorphism of local definitions can be handled. At the same time that we formalize the type system, we have made the effort of technically clarifying the overall process of type inference in a whole program. PublicationProgramming with non-determinism: a rewriting based approach(Universidad Complutense de Madrid, Servicio de Publicaciones, 2010-12-03) Rodríguez Hortalá, Juan; López Fraguas, Francisco Javier; Sánchez Hernández, JaimeEste trabajo trata acerca del uso del indeterminismo como un recurso expresivo de los lenguajes de programación. En los lenguajes indeterministas se ofrecen primitivas que pueden ser utilizadas para expresar cómputos cuyo resultado final no está totalmente determinado por los datos de entrada. En estos lenguajes, en los que la concurrencia no tiene porqué estar presente, el indeterminismo es parte del modelo de cómputo. La programación lógico-funcional, o en general, la programación declarativa multiparadigma, constituye un importante campo de investigación que intenta integrar en el mismo lenguaje las principales virtudes de varios paradigmas independientes: programación lógica, programación funcional perezosa e incluso programación con restricciones. Dos representantes modernos de esta linea son los lenguajes Toy y Curry, que comparten sus características principales. En estos lenguajes se emplean sistemas de reescritura de términos no confluentes como programas, de esta manera soportando funciones no estrictas e indeterministas, que son una de las características distintivas del paradigma. En esta tesis hemos intentado hacer algunas contribuciones al campo de la programación lógico-funcional indeterminista, usando los sistemas de reescritura basados en constructoras como el punto de partida de nuestros formalismos. Nuestros objetivos son diversos, a menudo al nivel de las descripciones semánticas, donde tratamos de aportar construcciones y resultados que esperamos puedan ser de utilidad para profundizar en la comprensión del significado de los programas, o como herramientas para la manipulación, análisis y transformación de programas. También nos hemos ocupado de aspectos más prácticos, y algunos prototipos han sido desarrollados a consecuencia de ello. Unas veces trabajamos en un marco consolidado---concretamente call-time choice o run-time choice---mientras que otras hemos decidido explorar las capacidades expresivas de las funciones indeterministas proponiendo nuevos marcos semánticos, algunos de ellos surgiendo de la combinación de semánticas ya existentes, otros presentando propuestas semánticas más novedosas. PublicationLiberal Typing for Functional Logic Programs(Springer, 2010) López Fraguas, Francisco; Martín Martín, Enrique; Rodríguez Hortalá, Juan; Ueda, K.We propose a new type system for functional logic programming which is more liberal than the classical Damas-Milner usually adopted, but it is also restrictive enough to ensure type soundness. Starting from Damas-Milner typing of expressions we propose a new notion of well-typed program that adds support for type-indexed functions, existential types, opaque higher-order patterns and generic functions-as shown by an extensive collection of examples that illustrate the possibilities of our proposal. In the negative side, the types of functions must be declared, and therefore types are checked but not inferred. Another consequence is that parametricity is lost, although the impact of this flaw is limited as "free theorems" were already compromised in functional logic programming because of non-determinism. PublicationRewriting and narrowing for constructor systems with call-time choice semantics(Cambridge University Press, 2014-03) López Fraguas, Francisco J.; Martín Martín, Enrique; Rodríguez Hortalá, Juan; Sánchez Hernández, JaimeNon-confluent and non-terminating constructor-based term rewrite systems are useful for the purpose of specification and programming. In particular, existing functional logic languages use such kind of rewrite systems to define possibly non-strict non-deterministic functions. The semantics adopted for non-determinism is call-time choice, whose combination with non-strictness is a non trivial issue, addressed years ago from a semantic point of view with the Constructor-based Rewriting Logic (CRWL), a well-known semantic framework commonly accepted as suitable semantic basis of modern functional logic languages. A drawback of CRWL is that it does not come with a proper notion of one-step reduction, which would be very useful to understand and reason about how computations proceed. In this paper we develop thoroughly the theory for the first order version of letrewriting, a simple reduction notion close to that of classical term rewriting, but extended with a let-binding construction to adequately express the combination of call-time choice with non-strict semantics. Let-rewriting can be seen as a particular textual presentation of term graph rewriting. We investigate the properties of let-rewriting, most remarkably their equivalence with respect to a conservative extension of the CRWL-semantics coping with let-bindings, and we show by some case studies that having two interchangeable formal views (reduction/semantics) of the same language is a powerful reasoning tool. After that, we provide a notion of let-narrowing which is adequate for call-time choice as proved by soundness and completeness results of let-narrowing with respect to letre writing. Moreover, we relate those let-rewriting and let-narrowing relations (and hence CRWL) with ordinary term rewriting and narrowing, providing in particular soundness and completeness of let-rewriting with respect to term rewriting for a class of programs which are deterministic in a semantic sense. PublicationVerification of the ROS NavFn planner using executable specification languages(Elsevier, 2023-04) Martin-Martin, Enrique; Montenegro Montes, Manuel; Riesco Rodríguez, Adrián; Rodríguez Hortalá, Juan; Rubio Cuéllar, Rubén RafaelThe Robot Operating System (ROS) is a framework for building robust software for complex robot systems in several domains. The Navigation Stack stands out among the different libraries available in ROS, providing a set of components that can be reused to build robots with autonomous navigation capabilities. This library is a critical component, as navigation failures could have catastrophic consequences for applications like self-driving cars where safety is crucial. Here we devise a general methodology for verifying this kind of complex systems by specifying them in different executable specification languages with verification support and validating the equivalence between the specifications and the original system using differential testing techniques. The complex system can then be indirectly analyzed using the verification tools of the specification languages like model checking, semi-automated functional verification based on Hoare logic, and other formal techniques. In this paper we apply this verification methodology to the NavFn planner, which is the main planner component of the Navigation Stack of ROS, using Maude and Dafny as specification languages. We have formally proved several desirable properties of this planner algorithm like the absence of obstacles in the planned path. Moreover, we have found counterexamples for other concerns like the optimality of the path cost.