Person:
Martín Martín, Enrique

Profile Picture
First Name
Enrique
Last Name
Martín Martín
URI
https://hdl.handle.net/20.500.14352/78704
Affiliation
Universidad Complutense de Madrid
Faculty / Institute
Informática
Department
Sistemas Informáticos y Computación
Area
Lenguajes y Sistemas Informáticos
Identifiers
UCM identifierORCIDScopus Author IDDialnet IDGoogle Scholar ID

Filters

20142
Reset filters

Settings

Start date: 2010 × Subject: 004.432.4 ×

Search Results

Now showing 1 - 2 of 2
  • Thumbnail Image
    Item
    Safe typing of functional logic programs with opaque patterns and local bindings
    (Information and Computation, 2014) López Fraguas, Francisco Javier; Martín Martín, Enrique; Rodríguez Hortalá, Juan
    Type 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.
  • Thumbnail Image
    Item
    Rewriting and narrowing for constructor systems with call-time choice semantics
    (Theory and Practice of Logic Programming, 2014) López Fraguas, Francisco Javier; Martín Martín, Enrique; Rodríguez Hortalá, Juan; Sánchez Hernández, Jaime
    Non-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.