Logic Programming Research Group
Functional Logic Programming

Sergio Antoy
Portland State University
USA

Editor: Enrico Pontelli

It is an honor to open this regular column of the newsletter on spotlights for research groups working in logic programming.  The research this spotlight addresses is Functional Logic (FL) programming.

FL programming integrates the functional and logic paradigms into a single language.  On the surface, a FL language may appear quite similar to a functional language, but it also provides the non-determinism, logic variables, and built-in search typical of logic languages.  FL languages are motivated by the observation that in a program most computations are functional, and it is convenient to code them as such, but sometimes logic features greatly simplify translating a problem into a program.

Curry is a FL language originating from an international initiative aiming at the definition and implementation of a lingua franca shared by the FL community for education, production and research.

A FL language is a functional language.  As such, it must provide the characterizing features of a modern functional language, such as higher-order functions, strong typing, algebraic datatype declarations, type inference, lazy evaluation, and monadic IO, to name a few.  For these reasons, Curry is syntactically very similar to Haskell.

A major problem of the integration of the functional and logic paradigms is how to evaluate an expression that contains unbound logic variables.  Narrowing offers an elegant solution to this problem.  Narrowing has some similarities with resolution in that it unifies terms, but it is defined for rewrite rules rather than Horn clauses.

I hope to give a feel of programming in a FL language with a couple of examples, in Curry.  The following conditional rule defines a function that returns the last element of a list:

       last l | l =:= x++[e] = e where x,e free

The condition of the rule, l =:= x++[e], is an equation in which l is the argument of the function, x and e are unbound variables, and ++ is the usual concatenation of lists.  Narrowing solves this equation and in the process binds the last element of l to e, which is the desired result.

A more interesting problem is to determine if a poker hand features a four-of-a-kind.  A card is represented by its suit and rank.  The operation rank returns the rank of a card.

    data Suit = Club | Spade | ...
    data Rank = Ace | King | ...
    data Card = Card Rank Suit
    rank (Card r _) = r

These declarations are legal Haskell code.  Thus, a poker hand is represented by a sequence of five cards.  The FL algorithm for this problem discards one non-deterministically chosen card from the hand and checks whether the rank of the remaining cards is the same.  The operator & is the conjunction of constraints.

    four hand = x++y:z =:= hand & map rank (x++z) =:= [r,r,r,r]
              where x,y,z,r free

The code is a straightforward implementation of the high-level FL algorithm.  The operation four takes a hand and succeeds if and only if the hand features a four-of-a-kind.  Variations that return the rank, r, and/or the discarded card, y, and/or the cards, x++z, witnessing the four-of-a-kind score are easy to obtain.

Narrowing solves constraints, equational and not, involving user defined algebraic types.  With a suitable strategy, narrowing ensures the soundness and the completeness of the computed solutions with varying degrees of optimality depending on the class of programs.

Research on narrowing-based FL programming languages is active. At Portland State University we are studying evaluation strategies for narrowing and architectures for the implementation of FL languages.  Most, if not all, current implementations are based on a formalism, called definitional trees, developed at PSU. Strategies and the proofs of their properties can be quite complex.  Worldwide, the following groups are most visible.  We apologize in advance for any omission.

Christian-Albrechts-Universität zu Kiel:
  Hanus, Brassel, Fischer, Huch
  Operational semantics, PAKCS implementation and tools

Portland State University, Portland, USA:
  Antoy, Brown
  Strategies & implementation

Universität Münster:
  Kuchen, Hermanns, Lux
  MCC implementation, declarative debugging

Universidad Complutense de Madrid:
  Rodriguez-Artalejo, Albert, Lopez-Fraguas, Caballero
  Sematics & implementation

Universidad Politècnica de Madrid:
  Moreno-Navarro, Gallego, Marino
  Semantics, Sloth implementation

Universidad Politècnica de Valencia:
  Alpuente, Escobar, Vidal
  Semantics, program transformation, debugging and verification