Functional logic programming
The functional logic programming is the union of the functional paradigm with the logic in a programming language. This includes most of the strong paradigm concepts, including higher order functions, non-deterministic execution, and unification. The pioneer of this creation was λProlog in the nineties. Other, newer functional logic programming languages are Curry and Mercury .
Basics
The examples are in the syntax of curry .
Functional programming
A functional program is a collection of functions or rules. A functional calculation consists of replacing partial expressions with equivalent partial expressions (taking the function definition into account) until replacements or reductions are no longer possible and a result is determined or a normal form is achieved. A partial expression that can be reduced is also referred to as a redex (from English reducible expression 'reducible expression' ). For the next examples, let the function be verdoppelndefined by
verdoppeln x = x + x
The expression verdoppeln 1is a redex and is replaced by 1 + 1, which in turn can be 2replaced by, whereby the +operator simplifies the concept of an infinite set of equations of the form 1 + 1 = 2, 1 + 2 = 3etc. Subexpressions can be evaluated in a similar way. In the example, the partial expression to be replaced is highlighted in italics.
verdoppeln (1 + 2) → (1 + 2) + (1 + 2) → 3 + (1 + 2) → 3 + 3 → 6
But there is also another order in which the expressions can be replaced:
verdoppeln (1 + 2) → verdoppeln 3 → 3 + 3 → 6
In this case, both evaluations lead to the same result. This property is called confluence and follows from the fundamental property of pure functional languages, referential transparency : the value of an expression to be determined does not depend on the order or the time of the evaluation (e.g. due to side effects). Hence, evidence is easier to maintain and the programs are easy to maintain.
Algebraic data types
Like functional languages, many functional logic languages support the definition of algebraic types by listing their constructors. For example, the data type Boolfor truth values is defined with the constructors Trueand Falseas follows:
data Bool = True | False
Functions whose parameters are such truth values can be defined by pattern matching , usually by several defining equations:
not True = False not False = True
The procedure to replace expressions with equivalents is still valid if the expressions have the appropriate form:
not (not False) → not True → False
More complicated data structures are represented by recursive data types. For example, a list above any type whose elements are of this type is either the empty list []or a non-empty list with a first element xand a remainder xs, represented by x : xs.
data List a = [] -- [] ist ein parameterloser Konstruktor (d. h. ein Literal), das die leere Liste darstellt. | a : List a -- Der Konstruktor wird infix notiert und ist der Doppelpunkt. -- Er hat zwei Parameter: ein Listenelement und ein Restglied, welches auch leer sein darf.
Usually one notes the type List awith [a]and finite lists x1 : x2 : … : xn : []with [x1, x2, …, xn]. Functions on recursive types can be defined inductively, whereby pattern matching enables convenient case differentiation. The concatenation can be defined as follows. The two concatenated lists must be of the same type. Variables for lists often end with S , cf. the plural formation in the English language.
(++) :: [a] -> [a] -> [a] -- Typdefinition: Zwei Listen mit gleichem Typ werden zu einer.
[] ++ ys = ys -- Leere Liste mit beliebiger Liste konkatenieren (x : xs) ++ ys = x : (xs ++ ys) -- Nicht-leere Liste rekursiv konkatenieren
Logical programming
Let it be the function lastthat returns the last element of a non-empty list for demonstration purposes. The following applies to all lists xsand elements e: last xs results eif and only if the ys ++ [e] same xsfor a suitable list ys.
Based on this specification, we can use logical programming techniques to define a function that fulfills this. Similar to logical languages, functional logical languages offer solutions for the search for existential quantified variables. In contrast to purely logical languages, they support the solving of equations with functional partial expressions, so that ys ++ [e] = [1, 2, 3]solving is done by instantiating yswith the list [1, 2]and ewith the value 3. Then it can lastbe defined as follows:
last :: [a] -> a last xs | ys ++ [e] =:= xs = e where ys, e free
The symbol =:=for equality conditions is used here to distinguish them syntactically from defining equality and comparisons. In a similar way, additional variables can be bound by where … freedeclaring them explicitly . The declaration is necessary and sensible to avoid typing errors. A conditional equation of the form L | B = Rcan be applied if the condition has been Bsolved. In contrast to purely functional languages, whose conditions can only be patterns or expressions of type Bool, functional-logic languages also support solving conditions by guessing the values of the unknowns in the condition; Pattern conditions are a special case of this. Restrictions that are explained below are used for this.
restrictions
Constraint is a mechanism by which a variable is bound to a value based on alternatives that are imposed by constraints. All possible values are tried in a certain order, with the rest of the program being called to verify that the binding is correct. Constraints are an extension of logic programming in that they yield a similar search, but it can produce values as part of the search rather than being limited to just checking.
Restricting is particularly useful because it enables functions such as relations to be handled; Values can be determined in a certain way in both directions. This is illustrated by the previous example, among other things.
As already noted, restrictions such as a reduction of the evaluation graph can be understood and there are often many different ways (strategies) to reduce a graph. Antoy et al. proved in the nineties that a certain strategy, the narrowing needed, is optimal to obtain a normal form with as few reductions as possible. Needed narrowing is a form of needs assessment , as opposed to Prolog's SLD resolution strategy .
Functional patterns
The rule with which the function was lastdefined above shows the fact that the actual argument ys ++ [e]must match the result of the expression , ysand eany values may be used for and . Since there is only one parameter on a page, this can alternatively be expressed in a very concise way:
last :: [a] -> a last (ys ++ [e]) = e
Purely functional languages do not allow such a definition, since the pattern on the left contains a defined function (namely the operator ++) that is not necessarily injective ; such a pattern is called a functional pattern. Functional patterns are created through the combination of functional and logical properties as well as the support of simple task definitions that require deep pattern comparisons in hierarchical structures. This example is ++generally not injective, since any non-empty list can be generated with [] ++ las well l ++ []; however, the free variables can only be selected in one way here, as they are subject to restrictions.
Nondeterminism
Since functional logic languages are able to solve equations containing function calls with unknown parameters, the execution system is based on nondeterministic calculations. This mechanism also enables the definition of non-deterministic operations that produce several different results on a given input. The mother of nondeterministic operations is the predefined infix operator ?, the selection operator, which nondeterministically returns one of its operands.
(?) :: a -> a -> a x ? y = x x ? y = y
Therefore, evaluating the expression returns 0 ? 1both 0and 1. Calculating with nondeterministic operations and calculating with free variables with restrictions have the same expressiveness.
The rules used to ?define them show an important characteristic of functional logic languages: all rules are attempted to evaluate a particular operation; in particular, the topmost realizable equation is not applied. Therefore you can with
insert :: a -> [a] -> [a] insert x ys = x : ys insert x (y : ys) = y : insert x ys
define an operation that inserts an element in an undefined position. In functional languages, the second equation would be unattainable because the first one can take all possible parameters. If the equations are reversed, the second equation would only be used for empty lists because the first applies to all non-empty lists. In functional logic programming, therefore, the principle of disregarding cases already treated in the equations above cannot be used; in this sense, each equation must be viewed as if it were on top.
With insert the function is permthrough
perm :: [a] -> [a] perm [] = [] perm (x : xs) = insert x (perm xs)
that returns each permutation of a given list.
supporting documents
- ↑ Gopalan Nadathur, D. Miller: Higher-Order Logic Programming . In: DM Gabbay, CJ Hogger, JA Robinson (eds.): Logic Programming (= Handbook of Logic in Artificial Intelligence and Logic Programming), Volume 5. Oxford University Press, 1998, ISBN 0198537921 , pp. 499-590.
- ↑ Sergio Antoy, Rachid Echahed and Michael Hanus: A Needed Narrowing Strategy . In: ACM (Ed.): Journal of the ACM . 47, No. 4, 2007, ISSN 0004-5411 , pp. 776-822. doi : 10.1145 / 347476.347484 .
- ↑ Sergio Antoy and Michael Hanus: Declarative Programming with Function Patterns, LOPSTR 2005 doi : 10.1007 / 11680093_2
- ↑ Sergio Antoy and Michael Hanus: Overlapping Rules and Logic Variables in Functional Logic Programs, International Conference on Logic Programming 2006 doi : 10.1007 / 11799573_9
Web links
- Functional logic programming at the University of Kiel