<?xml version="1.0" encoding="UTF-8"?>
<TEI xml:space="preserve" xmlns="http://www.tei-c.org/ns/1.0" 
xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" 
xsi:schemaLocation="http://www.tei-c.org/ns/1.0 https://raw.githubusercontent.com/kermitt2/grobid/master/grobid-home/schemas/xsd/Grobid.xsd"
 xmlns:xlink="http://www.w3.org/1999/xlink">
	<teiHeader xml:lang="en">
		<fileDesc>
			<titleStmt>
				<title level="a" type="main">Curry without Success</title>
			</titleStmt>
			<publicationStmt>
				<publisher/>
				<availability status="unknown"><licence/></availability>
			</publicationStmt>
			<sourceDesc>
				<biblStruct>
					<analytic>
						<author role="corresp">
							<persName><forename type="first">Sergio</forename><surname>Antoy</surname></persName>
							<email>antoy@cs.pdx.edu</email>
							<affiliation key="aff0">
								<orgName type="department">Computer Science Dept</orgName>
								<orgName type="institution">Portland State University</orgName>
								<address>
									<region>Oregon</region>
									<country key="US">U.S.A</country>
								</address>
							</affiliation>
						</author>
						<author>
							<persName><forename type="first">Michael</forename><surname>Hanus</surname></persName>
							<affiliation key="aff1">
								<orgName type="department">Institut für Informatik</orgName>
								<orgName type="institution">CAU Kiel</orgName>
								<address>
									<postCode>D-24098</postCode>
									<settlement>Kiel</settlement>
									<country key="DE">Germany</country>
								</address>
							</affiliation>
						</author>
						<title level="a" type="main">Curry without Success</title>
					</analytic>
					<monogr>
						<imprint>
							<date/>
						</imprint>
					</monogr>
					<idno type="MD5">8B5C09584BC1A7F273E5FF10DC7CD130</idno>
				</biblStruct>
			</sourceDesc>
		</fileDesc>
		<encodingDesc>
			<appInfo>
				<application version="0.7.2" ident="GROBID" when="2023-03-24T05:18+0000">
					<desc>GROBID - A machine learning software for extracting information from scholarly documents</desc>
					<ref target="https://github.com/kermitt2/grobid"/>
				</application>
			</appInfo>
		</encodingDesc>
		<profileDesc>
			<abstract>
<div xmlns="http://www.tei-c.org/ns/1.0"><p>Curry is a successful, general-purpose, functional logic programming language that predefines a singleton type Success explicitly to support its logic component. We take the likely-controversial position that without Success Curry would be as much logic or more. We draw a short history and motivation for the existence of this type and justify why its elimination could be advantageous. Furthermore, we propose a new interpretation of rule application which is convenient for programming and increases the similarity between the functional component of Curry and functional programming as in Haskell. We outline some related theoretical (semantics) and practical (implementation) consequences of our proposal.</p></div>
<div xmlns="http://www.tei-c.org/ns/1.0"><head n="1">Motivation</head><p>Recently, we coded a small Curry [16] module to encode and pretty-print JSON formatted documents <ref type="bibr" target="#b13">[14]</ref>. The JSON format encodes floating point numbers with a syntax that makes the decimal point optional. Our Curry System prints floating numbers with a decimal point. Thus, integers, which were converted to floats for encoding, were printed as floats, e.g., the integer value 2 was printed as "2.0". We found all those point-zeros annoying and distracting and decided to get rid of them. To avoid messing with the internal representation of numbers, and risking losing information, our algorithm would look for ".0" at the end of the string representation of a number in the JSON document and remove it. In the List library, we found a function, isSuffixOf, that tells us whether to drop the last two characters, but we did not find a function to drop the last 2 characters. How could we do that?</p><p>In the library we found the usual drop and take functions that work at the beginning of a string s. Hence, we could reverse s, drop 2 characters, and reverse again. We were not thrilled. Or we could take from s the first n − 2 characters, where n is the length of s. We were not thrilled either. In both cases, conceptually the string is traversed 3 times (probably in practice too) and extraneous functions are invoked. Not a big deal, but there must be a better way. Although the computation is totally functional, we started to think logic.</p><p>Curry has this fantastic feature called functional patterns <ref type="bibr" target="#b3">[4]</ref>. With it, we could code the following: fix int (x ++ ".0") = x</p><p>(1)</p></div>
			</abstract>
		</profileDesc>
	</teiHeader>
	<text xml:lang="en">
		<body>
<div xmlns="http://www.tei-c.org/ns/1.0"><p>Now we were thrilled! This is compact, simple and obviously correct. Of course, we would need a rule for cases in which the string representation of a number does not end in ".0", i.e.: fix int (x ++ ".0") = x fix int x = x</p><p>Without the last rule fix int would fail on a string such as "2.1". With the last rule the program would be incorrect because both rules would be applied for a number that ends in ".0". The latter is a consequence of the design decision that established that the order of the rules in a program is irrelevant-a major departure of Curry from popular functional languages. One of the reasons of this design decision is Success.</p></div>
<div xmlns="http://www.tei-c.org/ns/1.0"><head n="2">History</head><p>Putting it crudely, a functional logic language is a functional language extended with logic variables. The only complication of this extension is what to do when some function f is applied to some unbound logic variable u. There are two options, either to residuate on u or to narrow u. Residuation suspends the application of f, and computes elsewhere in the program in hopes that this computation will narrow u so that the suspended application of f can continue. Narrowing instantiates u to values that sustain the computation. For example, given the usual concatenation of lists: [] ++ ys = ys (x:xs) ++ ys = x : (xs ++ ys)</p><p>Narrowing u ++ t, where u is unbound and t is any expression, instantiates u to [] and u :us and continues these computations either one at the time or concurrently depending on the control strategy.</p><p>In early functional logic languages <ref type="bibr" target="#b0">[1,</ref><ref type="bibr" target="#b16">17]</ref>, in the tradition of logic programming, only predicates (as opposed to any function) are allowed to instantiate a logic variable. In the early days of Curry, we were not brave enough. Indiscriminate narrowing, such as that required for <ref type="bibr" target="#b0">(1)</ref>, which is based on (3), was uncharted territory and we decided that all functions would residuate except a small selected group called constraints. These functions are characterized by returning a singleton type called Success.</p><p>Narrowing has the remarkable property of solving equations <ref type="bibr" target="#b22">[23]</ref>. Indeed, the rule in <ref type="bibr" target="#b0">(1)</ref> works by solving an equation by narrowing. An application fix int(s), where s is a string, attempts to solve s = x++".0". A solution, "the" if any exists, gives the desired result x. Returning Success rather than Boolean, as the constrained equality does, had the desirable consequence that we would not "solve" an equation by deriving it to False, but had the drawback of introducing a new variant of equality, implemented in Curry by the operation "=:=", and the undesirable consequence that "some expressions were more equal than others" <ref type="bibr" target="#b18">[19]</ref>.</p><p>As a consequence of our hesitation, narrowing was limited to the arguments of constraints-a successful model well-established by Prolog. However, this model is at odds with a language with a functional component with normal (lazy) order of evaluation. Without functional nesting, there is no easy way to tell whether or not some argument of some constraint should be evaluated. Consider a program to solve the 8queens puzzle: permute x y = . . . succeed if y is a permutation of x safe y = . . . succeed if y is a safe placement of queens (4)</p><p>A solution of the puzzle is obtained by permute [1..8] y &amp;&amp; safe y, where y is likely a free variable. The constraint permute fully evaluates y upon returning even if safe may only look at the first two elements and determine that y is not safe. This prompted the invention of "non-deterministic functions", i.e., a function-like mechanism, that may return more than one value for the same combination of arguments, but is used as an ordinary function. With this idea, Example (4) is coded as: permute x = . . . return any permutation of x safe y = . . . as before <ref type="bibr" target="#b4">(5)</ref> In this case, a solution of the puzzle is obtained by safe y where y = permute [1 </p><p>The evaluation of permute [1..8] produces any permutation of <ref type="bibr">[1..8]</ref> only if both rules defining nd insert are applied when the second argument is a non-empty list. Thus, the well-established convention of functional languages that the first rule that matches an expression is the only one being fired had to be changed in the design of Curry.</p></div>
<div xmlns="http://www.tei-c.org/ns/1.0"><head n="3">Proposed Adjustments</head><p>Our modest proposal is to strip the Success type of any special meaning. Since Success is isomorphic to the Unit type, which is already defined in the Prelude, probably it becomes redundant. Future versions of the language could keep it for backward compatibility, but deprecate it. The first consequence of this change puts in question the usefulness of "=:=", the constrained equality. Equations can be solved using the Boolean equality "==" bringing Curry more in line with functional languages. To solve an equation by narrowing, we simply evaluate it using the standard rules defining Boolean equality. For example, below we show these rules for a polymorphic type List:</p><formula xml:id="formula_3">[] == [] = True (x:xs) == (y:ys) = x==y &amp;&amp; xs==ys [] == ( -: -) = False ( -: -) == [] = False<label>(7)</label></formula><p>However, we certainly want to avoid binding variables with instantiations that derive an equation to False since these bindings are not solutions. Avoiding these bindings is achieved with the following operation:</p><p>solve True = True <ref type="bibr" target="#b7">(8)</ref> and wrapping an equation with solve, i.e., to solve x = y, we code solve (x == y). Nostalgic programmers could redefine "=:=" as:</p><formula xml:id="formula_4">x =:= y = solve (x == y)<label>(9)</label></formula><p>When an equation occurs in the condition of a rule, the intended behavior is implied, i.e., the rule is fired only when the condition is (evaluates to) True.</p><p>In a short paragraph above, we find the symbols "=", "==" and "=:=". The first one is the (mathematical) equality. The other two are (computational) approximations of it with subtle differences. Our proposal simplifies this situation by having only "==" as the implementation of "=", as in functional languages, without sacrificing any of Curry's logic aspects.</p><p>The second consequence of our proposal is to review the rule selection strategy, i.e., the order, or more precisely its lack thereof, in which rules are fired. We have already hinted at this issue discussing example <ref type="bibr" target="#b1">(2)</ref>. Every rule that matches the arguments and satisfies the condition of a call is non-deterministically fired. A motivation for the independence of rule order was discussed in example <ref type="bibr" target="#b5">(6)</ref>. The ability of making non-deterministic choices is essential to functional logic programming, and it must be preserved, but it can be achieved in a different way.</p><p>The predefined operation "?" non-deterministically returns either of its arguments. This operation allows us to express non-determinism in a way different from rules with overlapping left-hand sides <ref type="bibr" target="#b2">[3]</ref>. For instance, the non-determinism of the operation nd insert in (6) can be moved from the left-hand sides of its defining rules to the right-hand sides as in the following definition: nd insert x ys = (x : ys) ? nd insert2 x ys nd insert2 x (y : ys) = y : nd insert x ys <ref type="bibr" target="#b9">(10)</ref> Indeed, some Curry compilers, like KiCS2 <ref type="bibr" target="#b7">[8]</ref>, implement this transformation. The definition of Curry at the time of this writing <ref type="bibr" target="#b15">[16]</ref> establishes that the order of the rules defining an operation is irrelevant. The same holds true for the conditions of a rule, except in the case in which the condition type is Boolean, and for flexible case expressions. Our next proposal is to change this design decision of Curry. Although this is somehow independent of our first proposal to remove the Success type, it is reasonable to consider both proposals at once since both simplify the use of Curry.</p><p>We propose to change the current definition of rule application in Curry as follows. To determine which rule(s) to fire for an application t = f (t 1 , . . . , t n ), where f is an operation and t 1 , . . . , t n are expressions, use the following strategy:</p><p>1. Scan the rules of f in textual order. An unconditional rule is considered as a conditional rule with condition True. 2. Fire the first rule whose left-hand side matches the application t and whose condition is satisfied. Ignore any remaining rule. 3. If no rule can be applied, the computation fails. 4. If a combination of arguments is non-deterministic, the previous points are executed independently for each non-deterministic choice of the combination of arguments.</p><p>In particular, if an argument is a free variable, it is non-deterministically instantiated to all its possible values.</p><p>As usual in a non-strict language like Curry, arguments of an operation application are evaluated as they are demanded by the operation's pattern matching and condition.</p><p>However, any non-determinism or failure during argument evaluation is not passed inside the condition evaluation. A precise definition of "inside" is in <ref type="bibr" target="#b5">[6,</ref><ref type="bibr">Def. 3]</ref>. This is quite similar to the behavior of set functions to encapsulate internal non-determinism <ref type="bibr" target="#b5">[6]</ref>. Apropos, we discuss in Section 5 how to exploit set functions to implement this concept.</p><p>Before discussing the advantages and implementation of this concept, we explain and motivate the various design decisions taken in our proposal. First, it should be noted that this concept distinguishes non-determinism outside and inside a rule application. If the condition of a rule has several solutions, this rule is applied if it is the first one with a true condition. Second, the computation proceeds non-deterministically with all the solutions of the condition. For instance, consider an operation to look up values for keys in an association list:</p><formula xml:id="formula_5">lookup key assoc | assoc == ( -++ [(key,val)] ++ -) = Just val</formula><p>where val free lookup --= Nothing <ref type="bibr" target="#b10">(11)</ref> If we evaluate lookup 2 [(2, 14), <ref type="bibr" target="#b2">(3,</ref><ref type="bibr" target="#b16">17)</ref>, <ref type="bibr" target="#b1">(2,</ref><ref type="bibr" target="#b17">18)</ref>], the condition of the first rule is solvable. Thus, we ignore the remaining rules and apply only the first rule to evaluate this expression. Since the condition has the two solutions {val → 14} and {val → 18}, we yield the values Just 14 and Just 18 for this expression. Note that this is in contrast to Prolog's if-then-else construct which checks the condition only once and proceeds just with the first solution of the condition. If we evaluate lookup 2 [ <ref type="bibr" target="#b2">(3,</ref><ref type="bibr" target="#b16">17)</ref>], the condition of the first rule is not solvable but the second rule is applicable so that we obtain the result Nothing.</p><p>On the other hand, non-deterministic arguments might trigger different rules to be applied. Consider the expression lookup (2?3) [ <ref type="bibr" target="#b2">(3,</ref><ref type="bibr" target="#b16">17)</ref>]. Since the non-determinism in the arguments leads to independent rule applications (see item 4), this expression leads to independent evaluations of lookup 2 [ <ref type="bibr" target="#b2">(3,</ref><ref type="bibr" target="#b16">17)</ref>] and lookup 3 <ref type="bibr">[(3, 17)</ref>]. The first one yields Nothing, whereas the second one yields Just 17.</p><p>Similarly, free variables as arguments might lead to independent results since free variables are equivalent to non-deterministic values <ref type="bibr" target="#b4">[5]</ref>. For instance, the expression lookup 2 xs yields the value Just v with the binding {xs → (2, v): }, but also the value Nothing with the binding {xs → []} (as well as many other solutions). Again, this behavior is different from Prolog's if-then-else construct which performs bindings for free variables inside the condition independently of its source. In contrast to Prolog, our design supports completeness in logic-oriented computations even in the presence of if-then-else.</p><p>The latter desirable property has also implications for the handling of failures occurring when arguments are evaluated. For instance, consider the expression "lookup 2 failed" (where failed is a predefined operation which always fails whenever it is evaluated). Because the evaluation of the condition of the first rule fails, the entire expression evaluation fails instead of returning the value Nothing. This is motivated by the fact that we need the value of the association list in order to check the satisfiability of the condition, but this value is not available.</p><p>To see the consequences of an alternative design decision, consider the following contrived definition of an operation that checks whether its argument is the unit value () (which is the only value of the unit type):</p><formula xml:id="formula_6">isUnit x | x == () = True isUnit -= False<label>(12)</label></formula><p>In our proposal, the evaluation of isUnit failed fails. In an alternative design (like Prolog's if-then-else construct), one might skip any failure during condition checking and proceed with the next rule. In this case, we would return the value False for the expression isUnit failed. This is quite disturbing since the (deterministic!) operation isUnit, which has only one possible input value, could return two values: True for the call isUnit () and False for the call isUnit failed. Moreover, if we call this operation with a free variable, like isUnit x, we obtain the single binding {x → ()} and value True (since free variables are never bound to failures). Thus, either our semantics would be incomplete for logic computations or we compute too many values. In order to get a consistent behavior, we require that failures of arguments demanded for condition checking lead to failures of evaluations.</p><p>Changing the meaning of rule selection from an order-independent semantics to a sequential interpretation is an important change in the design of Curry. However, this change is relevant only for a relatively small amount of existing programs. First, most of the operations in a functional logic program are inductively sequential <ref type="bibr" target="#b1">[2]</ref>, i.e., they are defined by rules where the left-hand sides do not overlap. Hence, the order of the rules does not affect the definition of such operations. Second, rules defined with traditional Boolean guards residuate if they are applied to unknown arguments, i.e., it is usually not intended to apply alternative conditions to a given call. This fits to a sequential interpretation of conditions. Moreover, our proposal supports the use of conditional rules in a logic programming manner with unknown arguments, since this "outside" non-determinism does not influence the sequential condition checking.</p><p>Nevertheless, there are also cases where a sequential interpretation of rules is not intended, e.g., in a rule-oriented programming style, which is often used in knowledgebased or constraint programming. Although we argued that one can always translate overlapping patterns into rules with non-overlapping patterns by using the choice operator "?", the resulting code might be less readable. Finally, we have to admit that in a declarative language ignoring the order of the rules is more elegant though not always as convenient. Hence, a good compromise would be a compiler pragma that allows to choose between a sequential or an unordered interpretation of overlapping rules.</p></div>
<div xmlns="http://www.tei-c.org/ns/1.0"><head n="4">Advantages</head><p>In this section we justify through exemplary problems the advantages of the proposed changes.</p><p>Example 1. With the proposed semantics, (2) is a simple and obviously correct solution of the problem, discussed in the introduction, of "fixing" the representation of integers in a JSON document.</p><p>Example 2. As in the previous example, our proposed semantics is compatible with functional patterns. Hence, <ref type="bibr" target="#b10">(11)</ref> can be more conveniently coded as:</p><p>lookup key ( -++ [(key,val)] ++ -) = Just val lookup --= Nothing (13)</p><p>Example 3. Consider a read-eval-print loop of a functional logic language such as Curry. A top-level expression may contain free variables that are declared by a free clause such as in the following example:</p><p>x ++ y == <ref type="bibr" target="#b0">[1,</ref><ref type="bibr" target="#b1">2,</ref><ref type="bibr" target="#b2">3,</ref><ref type="bibr" target="#b3">4]</ref> where x, y free</p><p>Of course, the free clause is absent if there are no free variables in the top-level expression. The free variables, when present, are easily extracted with a "deep" pattern as follows: breakFree (exp++" where "++wf++" free")) = (exp,wf) breakFree exp = (exp,"")</p><p>For this code to work, the rules of breakFree must be tried in order and the second one must be fired only if the first one fails. Example 4. Suppose that World Cup soccer scores are represented in either of the following forms:</p><p>GER -: -USA GER 1:0 USA</p><p>where the first line represents a game not yet played and the second one a game in which the digits are the goals scored by the adjacent team (a single digit suffices in practice).</p><p>The following operation parses scores:</p><p>parse (team1++" -: -"++team2) = (team1,team2,Nothing) parse (team1++[' ',x,':',y,' ']++team2) | isDigit x &amp;&amp; isDigit y = (team1,team2, Just (toInt x,toInt y)) parse -= error "Wrong format!" <ref type="bibr" target="#b16">(17)</ref> Example 5. The Dutch National Flag problem <ref type="bibr" target="#b12">[13]</ref> has been proposed in a simple form to discuss the termination of rewriting <ref type="bibr" target="#b11">[12]</ref>. A formulation in Curry of this simple form is equally simple:</p><formula xml:id="formula_10">dnf (x++[White,Red]++y) = dnf (x++[Red,White]++y) dnf (x++[Blue,Red]++y) = dnf (x++[Red,Blue]++y) dnf (x++[Blue,White]++y) = dnf (x++[White,Blue]++y)<label>(18)</label></formula><p>However, <ref type="bibr" target="#b17">(18)</ref> needs a termination condition to avoid failure. With our proposed semantics, this condition is simply:</p><formula xml:id="formula_11">dnf x = x<label>(19)</label></formula><p>With the standard semantics, a much more complicated condition is needed.</p></div>
<div xmlns="http://www.tei-c.org/ns/1.0"><head n="5">Implementation</head><p>A good implementation of the proposed changes in the semantics of rule selection requires new compilation schemes for Curry. However, an implementation can also be obtained by a transformation over source programs when existing advanced features of Curry are exploited. This approach provides a reference semantics that avoids explicitly specifying all the details of our proposal, in particular, the subtle interplay between condition solving and non-determinism and failures in arguments. Hence, we define in this section a program transformation that implements our proposed changes within existing Curry systems. Initially, we discuss the implementation of a single rule with a sequence of conditions, i.e., a program rule of the form</p><formula xml:id="formula_12">l | c 1 = e 1 . . . | c k = e k<label>(20)</label></formula><p>According to our proposal, if the left-hand side l matches a call, the conditions c 1 , . . . , c k are sequentially evaluated. If c i is the first condition that evaluates to True, all other conditions are ignored so that (20) becomes equivalent to</p><formula xml:id="formula_13">l | c i = e i</formula><p>Note that the subsequent conditions are ignored even if the condition c i also evaluates to False. Thus, the standard translation of rules with multiple guards, as defined in the current report of Curry <ref type="bibr" target="#b15">[16]</ref>, i.e., replacing multiple guards by nested if-then-else constructs, would yield a non-intended semantics. Moreover, non-determinism and failures in the evaluation of actual arguments must be distinguished from similar outcomes caused by the evaluation of the condition, as discussed in Section 3. All these requirements call for the encapsulation of condition checking where "inside" and "outside" non-determinism are distinguished and handled differently. Fortunately, recent developments for encapsulated search in functional logic programming <ref type="bibr" target="#b5">[6,</ref><ref type="bibr" target="#b9">10]</ref> provide an appropriate solution of this problem. For instance, <ref type="bibr" target="#b9">[10]</ref> proposes an encapsulation primitive allValues so that the expression (allValues e) evaluates to the set of values of e where only internal non-determinism inside e is considered. Thus, we can use the following expression to check a condition c with our intended meaning: <ref type="foot" target="#foot_0">3</ref>if notEmpty (allValues (solve c)) then e 1 else e 2 <ref type="bibr" target="#b20">(21)</ref> According to <ref type="bibr" target="#b9">[10]</ref>, the meaning of this expression is as follows:</p><p>1. Test whether there is some evaluation of c to True.</p><p>2. If the test is positive, evaluate e 1 .</p><p>3. If there is no evaluation of c to True, evaluate e 2 .</p><p>The semantics of allValues ensures that non-determinism and failures caused by expressions not defined inside c, in particular, parameters of the left-hand side l of the operation, are not encapsulated. The Curry implementations PAKCS <ref type="bibr" target="#b14">[15]</ref> and KiCS2 <ref type="bibr" target="#b7">[8]</ref> provide set functions <ref type="bibr" target="#b5">[6]</ref> instead of allValues which allows the implementation of this conditional in a similar way.</p><p>Our expected semantics demands that a rule with a solvable condition be applied for each true condition, in particular, with a possible different binding computed by evaluating the condition. To implement this behavior, we assume an auxiliary operation ifTrue that combines a condition and an expression. This operation is simply defined by</p><formula xml:id="formula_14">ifTrue True x = x<label>(22)</label></formula><p>Then we define the meaning of ( <ref type="formula" target="#formula_12">20</ref>) by the following transformation:</p><formula xml:id="formula_15">l = if notEmpty (allValues (solve c 1 )) then (ifTrue c 1 e 1 ) else . . . if notEmpty (allValues (solve c k )) then (ifTrue c k e k ) else failed<label>(23)</label></formula><p>There are obvious simplifications of this general scheme. For instance, if c k = True, as frequently is the case, the last line of ( <ref type="formula" target="#formula_15">23</ref>) becomes e k . This transformation scheme is mainly intended as the semantics of sequential condition checking rather than as the final implementation (similarly to the specification of the meaning of guards in Haskell <ref type="bibr" target="#b19">[20]</ref>). A sophisticated implementation could improve the actual code. For instance, each condition c i is duplicated in our scheme. Moreover, it seems that conditions are always evaluated twice. However, this is not the case if a lazy implementation of encapsulated search via allValues or set functions is used, as in the Curry implementation KiCS2 <ref type="bibr" target="#b9">[10]</ref>. If c i is the first solvable condition, the emptiness test for (allValues c i ) can be decided after computing a first solution. In this case, this solution is computed again (and now also all other solutions) in the then-part in order to pass its computed bindings to e i . Of course, a more primitive implementation might avoid this duplicated evaluation.</p><p>Next we consider the transformation of a sequence of rules</p><formula xml:id="formula_16">l 1 r 1 . . . l k r k (24)</formula><p>where each left-hand side l i is a pattern f p i1 . . . p ini for the same function f and each r i is a sequence of condition/expression pairs of the form "| c = e" as shown in <ref type="bibr" target="#b19">(20)</ref>. <ref type="foot" target="#foot_1">4</ref>We assume that the pattern arguments p ij contain only constructors and variables. In particular, functional patterns have been eliminated by moving them into the condition using the function pattern unification operator "=:&lt;=" (as shown in <ref type="bibr" target="#b3">[4]</ref>). For instance, rule ( <ref type="formula">1</ref>) is transformed into</p><formula xml:id="formula_17">fix int xs | (x ++ ".0") =:&lt;= xs = x (25)</formula><p>Finally, we assume that subsequent rules with the same pattern (up to variable renaming) are joined into a single rule with multiple guards. For instance, the rules (2) can be joined (after eliminating the functional pattern) into the single rule -The patterns in the left-hand sides l 1 , . . . , l k are inductively sequential <ref type="bibr" target="#b1">[2]</ref>, i.e., the patterns can be organized in a tree structure such that there is always a discriminating (inductive) argument: since there are no overlapping left-hand sides in this case, the order of the rules is not important for the computed results. Therefore, no further transformation is necessary in this case. Note that most functions in typical functional logic programs are defined by inductively sequential rules. -Otherwise, there might be overlapping left-hand sides so that it is necessary to check all rules in a sequential manner. For this purpose, we put the pattern matching into the condition so that the patterns and conditions are checked together. Thus, a rule like</p><formula xml:id="formula_18">f p 1 . . . p n | c = e is transformed into f x 1 . . . x n | (\p 1 . . . p n -&gt; c ) x 1 . . . x n = (\p 1 . . . p n -&gt; ifTrue c e) x 1 . . . x n</formula><p>where x 1 , . . . , x n are fresh variables (the extension to rules with multiple conditions is straightforward). Using this transformation, we obtain a list of rules with identical left-hand sides which can be joined into a single rule with multiple guards, as described above. </p><p>For an example of transforming rules with overlapping patterns, consider an operation that reverses a two-element list and leaves all other lists unchanged:</p><formula xml:id="formula_20">rev2 [x,y] = [y,x] rev2 xs = xs<label>(28)</label></formula><p>According to our transformation, this definition is mapped into (after some straightforward simplifications):</p><formula xml:id="formula_21">rev2 xs = if notEmpty (allValues (\[x,y] -&gt; True) xs) then (\[x,y] -&gt; [y,x]) xs else xs<label>(29)</label></formula><p>Thanks to the logic features of Curry, one can also use this definition to generate appropriate argument values for rev2. For instance, if we evaluate the expression rev2 xs (where xs is a free variable), the Curry implementation KiCS2 <ref type="bibr" target="#b7">[8]</ref> has a finite search space and computes the following bindings and values:</p><formula xml:id="formula_22">{xs = []} [] {xs = [x1]} [x1] {xs = [x1,x2]} [x2,x1] {xs = (x1:x2:x3:x4)} (x1:x2:x3:x4)</formula><p>As mentioned above, the transformation presented in this section is intended to serve as a reference semantics for our proposed changes and to provide a prototypical implementation. There are various possibilities to improve this implementation. For instance, if the right-hand side expressions following each condition are always evaluable to a value, i.e., to a finite expression without defined operations, the duplication of the code of the condition as well as the potential double evaluation of the first solvable condition can be easily avoided. As an example, consider the following operation that checks whether a string contains a non-negative float number (without an exponent):</p><formula xml:id="formula_23">isNNFloat (f1 ++ "." ++ f2) | all isDigit f1 &amp;&amp; all isDigit f2 = True isNNFloat -= False (30) If c denotes the condition (f1 ++ "." ++ f2) =:&lt;= s &amp;&amp; all isDigit f1 &amp;&amp; all isDigit f2<label>(31)</label></formula><p>by functional pattern elimination <ref type="bibr" target="#b3">[4]</ref>, program (30) is equivalent to</p><formula xml:id="formula_24">isNNFloat s | c = True isNNFloat -= False<label>(32)</label></formula><p>Applying our transformation, we obtain the following code with the duplicated condition c: isNNFloat s = if notEmpty (allValues (solve c)) then (ifTrue c True) else False</p><p>Since the expressions on the right-hand side are always values (True or False), we can put these expressions into the sets computed by allValues. Then the check for a solvable condition becomes equivalent to check the non-emptiness of these value sets so that we return non-deterministically some value of this set. <ref type="foot" target="#foot_2">5</ref> This idea can be implemented by the following scheme which does not duplicate the condition and evaluates it only once (the actual code can be simplified but we want to show the general scheme):</p><p>isNNFloat s = if notEmpty s1 then chooseValue s1 else False where s1 = allValues (ifTrue c True)</p><formula xml:id="formula_26">(34)</formula><p>Note that this optimization is not applicable if it is not ensured that the right-hand side expressions are always evaluable to values. For instance, consider definition (28) of rev2 and the expression head (rev2 [nv, 0]), where nv is an expression without a value (e.g., failure or non-termination). With our current transformation (29), we compute the value 0 for this expression. However, the computation of the set of all values of (rev2 [nv, 0]) w.r.t. the first rule defining rev2 does not yield any set since the righthand side [0, nv] has no value. This explains our transformation scheme <ref type="bibr" target="#b22">(23)</ref> which might look complicated at a first glance. However, there is another transformation to implement overlapping rules like (28) with our intended semantics. If the rules are unconditional, one can "complete" the missing constructor patterns in order to obtain an inductively sequential definition. For the operation rev2, we obtain the following definition: </p><p>Since a case can be more efficiently executed than an encapsulated computation, this alternative transformation might lead to larger but more efficient target code.</p></div>
<div xmlns="http://www.tei-c.org/ns/1.0"><head n="6">Related Work</head><p>Declarative programming languages support the construction of readable and reliable programs by partitioning complex procedures into smaller units-mainly using case distinction by pattern matching and conditional rules. Since we propose a new interpretation of case distinctions for functional logic programs, we compare our proposal with existing ones with similar objectives. The functional programming language Haskell <ref type="bibr" target="#b19">[20]</ref> provides, similarly to Curry, also pattern matching and guarded rules for case distinctions. Our proposal for a new sequential interpretation of patterns increases the similarities between Curry and Haskell. Although Curry provides more features due to the built-in support to deal with nondeterministic and failing computations, our proposal is a conservative extension of Haskell's guarded rules, i.e., it has the same behavior as Haskell when non-determinism and failures do not occur. To see this, consider a program rule with multiple conditions:</p><formula xml:id="formula_28">l | c 1 = e 1 . . . | c k = e k<label>(36)</label></formula><p>Since non-deterministic computations do not exist in Haskell and failures lead to exceptions in Haskell, we assume that, if this rule is applied in Haskell to an expression e, there is one condition c i which evaluates to True and all previous conditions c 1 , . . . , c i−1 evaluate to False. If we consider the same rule translated with the transformation scheme <ref type="bibr" target="#b22">(23)</ref>, obviously each condition notEmpty (allValues (solve c j )) reduces to False for j = 1, . . . , i − 1 and to True for j = i. Thus, the application of this rule reduces e to (ifTrue c i e i ) and, subsequently, to e i , as in Haskell.</p><p>The logic programming language Prolog <ref type="bibr" target="#b10">[11]</ref> also supports pattern matching and, for sequential conditions, an if-then-else construct of the form "c -&gt; e 1 ; e 2 ". Although Prolog can deal, similarly to Curry, with non-deterministic and failing compu-tations, the if-then-else construct usually restricts the completeness of the search space due to cutting the choice points created by c before executing e 1 . Hence, only the first solution of c is used to evaluate e 1 . Furthermore, inside and outside non-determinism is not distinguished so that variables outside the condition c might be bound during its evaluation. This has the effect that predicates where if-then-else is used are often restricted to a particular mode. For instance, consider the re-definition of rev2 (28) as a predicate in Prolog using if-then-else:</p><formula xml:id="formula_29">rev2(Xs,Ys) :-Xs=[X,Y] -&gt; Ys=[Y,X] ; Ys=Xs.<label>(37)</label></formula><p>If we try to solve the goal rev2(Xs, Ys), Prolog yields the single answer Xs = [A, B], Ys = [B, A]. Thus, in contrast to our approach, all other answers are lost. Various encapsulation operators have been proposed for functional logic programs <ref type="bibr" target="#b6">[7]</ref> to encapsulate non-deterministic computations in some data structure. Set functions <ref type="bibr" target="#b5">[6]</ref> have been proposed as a strategy-independent notion of encapsulating nondeterminism to deal with the interactions of laziness and encapsulation (see <ref type="bibr" target="#b6">[7]</ref> for details). We can also use set functions to distinguish successful and non-successful computations, similarly to negation-as-failure in logic programming, exploiting the possibility to check result sets for emptiness. When encapsulated computations are nested and performed lazily, it turns out that one has to track the encapsulation level in order to obtain intended results, as discussed in <ref type="bibr" target="#b9">[10]</ref>. Thus, it is not surprising that set functions and related operators fit quite well to our proposal.</p><p>Computations with failures for the implementation of an if-then-else construct and default rules in functional logic programs have been also explored in <ref type="bibr" target="#b17">[18,</ref><ref type="bibr" target="#b21">22]</ref>. In these works, an operator, fails, is introduced to check whether every reduction of an expression to a head-normal form is not successful. The authors show that this operator can be used to define a single default rule, but not the more general sequential rule checking of our approach. Moreover, nested computations with failures are not considered by these works. As a consequence, the operator fails might yield unintended results if it is used in nested expressions. For instance, if we use fails instead of allValues to implement the operation isUnit defined in <ref type="bibr" target="#b11">(12)</ref>, the evaluation of isUnit failed yields the value False in contrast to our intended semantics.</p></div>
<div xmlns="http://www.tei-c.org/ns/1.0"><head n="7">Conclusions</head><p>We proposed two changes to the current design of Curry. The first one concerns the removal of the type Success and the related constraint equality "=:=". This simplifies the language since it relieves the programmer from choosing the appropriate equality operator. The second one concerns a strict order in which rules and conditions are tried to reduce an expression. This makes the language design more similar to functional languages like Haskell so that functional programmers will be more comfortable with Curry. Nevertheless, the logic programming features, like non-determinism and evaluating functions with unknown arguments, are still applicable with our new semantics. This distinguishes our approach from similar concepts in logic programming which simply cuts alternatives.</p><p>However, our proposal comes also with some drawbacks. We already mentioned that in knowledge-based or constraint programming applications, a sequential ordering of rules is not intended. Hence, a compiler pragma could allow the programmer to choose between a sequential or an unordered interpretation of overlapping rules.</p><p>A further drawback of our approach concerns the run-time efficiency. We argued that solving "==" equations by narrowing with standard equational rules can replace the constraint equality "=:=". Although this is true from a semantic point of view, the constraint equality operator "=:=" is more efficient from an operational point of view. If x and y are free variables, the equational constraint "x=:=y" is deterministically solved by binding x to y (or vice versa), whereas the Boolean equality "x==y" is solved by non-deterministically instantiating x and y to identical values. The efficiency improvement of performing is well known, e.g., it is benchmarked in <ref type="bibr" target="#b8">[9]</ref> for the Curry implementation KiCS2. On the other hand, the Boolean equality "x==y" is more powerful since it can also solve negated conditions, i.e., evaluate "x==y" to False by binding x and y to different values.</p><p>Hence, for future work it is interesting to find a compromise, e.g., performing variable bindings when "x==y" should be reduced to True without any surrounding negations. A program analysis could be useful to detect such situations at compile time.</p><p>Finally, the concurrency features of Curry must be revised. Currently, concurrency is introduced by the concurrent conjunction operator "&amp;" on constraints. If the constraint type Success is removed, other forms of concurrent evaluations might be introduced, e.g., in operators with more than one demanded argument ("==", "+",. . . ), explicit concurrent Boolean conjunctions, or only in the I/O monad similarly to Concurrent Haskell <ref type="bibr" target="#b20">[21]</ref>.</p><p>Despite all the drawbacks, our proposal is a reasonable approach to simplify the design of Curry and make it more convenient for the programmer.</p></div><figure xmlns="http://www.tei-c.org/ns/1.0" xml:id="fig_1"><head>For</head><label></label><figDesc>instance, the definition of fix int (26) is transformed into fix int xs = if notEmpty (allValues (solve (x++".0" =:&lt;= xs))) then (ifTrue (x++".0" =:&lt;= xs) x) else xs</figDesc></figure>
<figure xmlns="http://www.tei-c.org/ns/1.0" xml:id="fig_2"><head></head><label></label><figDesc>rev2 [x,y] = [y,x] rev2 [] = [] rev2 [x] = [x]rev2 (x:y:z:xs) = x:y:z:xs</figDesc></figure>
			<note xmlns="http://www.tei-c.org/ns/1.0" place="foot" n="3" xml:id="foot_0"><ref type="bibr" target="#b9">[10]</ref> defines only an operation isEmpty. Hence we assume that notEmpty is defined by the rule notEmpty x = not (isEmpty x).</note>
			<note xmlns="http://www.tei-c.org/ns/1.0" place="foot" n="4" xml:id="foot_1">In order to handle all rules in a unique manner, we consider an unconditional rule "li = ei" as an abbreviation for the conditional rule "li | True = ei".</note>
			<note xmlns="http://www.tei-c.org/ns/1.0" place="foot" n="5" xml:id="foot_2">The predefined operation chooseValue non-deterministically returns some value of a set.</note>
		</body>
		<back>

			<div type="acknowledgement">
<div xmlns="http://www.tei-c.org/ns/1.0"><head n="8">Acknowledgments</head><p>This material is based upon work partially supported by the National Science Foundation under Grant No. CCF-1317249.</p></div>
			</div>

			<div type="references">

				<listBibl>

<biblStruct xml:id="b0">
	<analytic>
		<title level="a" type="main">Towards a meaning of LIFE</title>
		<author>
			<persName><forename type="first">H</forename><surname>Aït-Kaci</surname></persName>
		</author>
		<author>
			<persName><forename type="first">A</forename><surname>Podelski</surname></persName>
		</author>
	</analytic>
	<monogr>
		<title level="m">Proc. of the 3rd Int. Symposium on Programming Language Implementation and Logic Programming</title>
				<meeting>of the 3rd Int. Symposium on Programming Language Implementation and Logic Programming</meeting>
		<imprint>
			<date type="published" when="1991">1991</date>
			<biblScope unit="volume">528</biblScope>
			<biblScope unit="page" from="255" to="274" />
		</imprint>
	</monogr>
</biblStruct>

<biblStruct xml:id="b1">
	<analytic>
		<title level="a" type="main">Definitional trees</title>
		<author>
			<persName><forename type="first">S</forename><surname>Antoy</surname></persName>
		</author>
	</analytic>
	<monogr>
		<title level="m">Proc. of the 3rd International Conference on Algebraic and Logic Programming</title>
				<meeting>of the 3rd International Conference on Algebraic and Logic Programming</meeting>
		<imprint>
			<date type="published" when="1992">1992</date>
			<biblScope unit="volume">632</biblScope>
			<biblScope unit="page" from="143" to="157" />
		</imprint>
	</monogr>
</biblStruct>

<biblStruct xml:id="b2">
	<analytic>
		<title level="a" type="main">Optimal non-deterministic functional logic computations</title>
		<author>
			<persName><forename type="first">S</forename><surname>Antoy</surname></persName>
		</author>
		<ptr target="http://cs.pdx.edu/∼antoy/homepage/publications/alp97/full.pdf" />
	</analytic>
	<monogr>
		<title level="m">Proceedings of the Sixth International Conference on Algebraic and Logic Programming (ALP&apos;97)</title>
				<meeting>the Sixth International Conference on Algebraic and Logic Programming (ALP&apos;97)<address><addrLine>Southampton, UK</addrLine></address></meeting>
		<imprint>
			<publisher>Springer</publisher>
			<date type="published" when="1298">September 1997. 1298</date>
			<biblScope unit="page" from="16" to="30" />
		</imprint>
	</monogr>
</biblStruct>

<biblStruct xml:id="b3">
	<analytic>
		<title level="a" type="main">Declarative programming with function patterns</title>
		<author>
			<persName><forename type="first">S</forename><surname>Antoy</surname></persName>
		</author>
		<author>
			<persName><forename type="first">M</forename><surname>Hanus</surname></persName>
		</author>
	</analytic>
	<monogr>
		<title level="m">Proceedings of the International Symposium on Logic-based Program Synthesis and Transformation (LOP-STR&apos;05)</title>
		<title level="s">LNCS</title>
		<meeting>the International Symposium on Logic-based Program Synthesis and Transformation (LOP-STR&apos;05)</meeting>
		<imprint>
			<publisher>Springer</publisher>
			<date type="published" when="2005">2005</date>
			<biblScope unit="volume">3901</biblScope>
			<biblScope unit="page" from="6" to="22" />
		</imprint>
	</monogr>
</biblStruct>

<biblStruct xml:id="b4">
	<analytic>
		<title level="a" type="main">Overlapping rules and logic variables in functional logic programs</title>
		<author>
			<persName><forename type="first">S</forename><surname>Antoy</surname></persName>
		</author>
		<author>
			<persName><forename type="first">M</forename><surname>Hanus</surname></persName>
		</author>
	</analytic>
	<monogr>
		<title level="m">Proceedings of the 22nd International Conference on Logic Programming (ICLP 2006)</title>
				<meeting>the 22nd International Conference on Logic Programming (ICLP 2006)</meeting>
		<imprint>
			<date type="published" when="2006">2006</date>
			<biblScope unit="volume">4079</biblScope>
			<biblScope unit="page" from="87" to="101" />
		</imprint>
	</monogr>
</biblStruct>

<biblStruct xml:id="b5">
	<analytic>
		<title level="a" type="main">Set functions for functional logic programming</title>
		<author>
			<persName><forename type="first">S</forename><surname>Antoy</surname></persName>
		</author>
		<author>
			<persName><forename type="first">M</forename><surname>Hanus</surname></persName>
		</author>
	</analytic>
	<monogr>
		<title level="m">Proceedings of the 11th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP&apos;09)</title>
				<meeting>the 11th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP&apos;09)</meeting>
		<imprint>
			<publisher>ACM Press</publisher>
			<date type="published" when="2009">2009</date>
			<biblScope unit="page" from="73" to="82" />
		</imprint>
	</monogr>
</biblStruct>

<biblStruct xml:id="b6">
	<analytic>
		<title level="a" type="main">Encapsulating non-determinism in functional logic computations</title>
		<author>
			<persName><forename type="first">B</forename><surname>Braßel</surname></persName>
		</author>
		<author>
			<persName><forename type="first">M</forename><surname>Hanus</surname></persName>
		</author>
		<author>
			<persName><forename type="first">F</forename><surname>Huch</surname></persName>
		</author>
	</analytic>
	<monogr>
		<title level="j">Journal of Functional and Logic Programming</title>
		<imprint>
			<biblScope unit="issue">6</biblScope>
			<date type="published" when="2004">2004. 2004</date>
		</imprint>
	</monogr>
</biblStruct>

<biblStruct xml:id="b7">
	<analytic>
		<title level="a" type="main">KiCS2: A new compiler from Curry to Haskell</title>
		<author>
			<persName><forename type="first">B</forename><surname>Braßel</surname></persName>
		</author>
		<author>
			<persName><forename type="first">M</forename><surname>Hanus</surname></persName>
		</author>
		<author>
			<persName><forename type="first">B</forename><surname>Peemöller</surname></persName>
		</author>
		<author>
			<persName><forename type="first">F</forename><surname>Reck</surname></persName>
		</author>
	</analytic>
	<monogr>
		<title level="m">Proc. of the 20th International Workshop on Functional and (Constraint) Logic Programming</title>
				<meeting>of the 20th International Workshop on Functional and (Constraint) Logic Programming<address><addrLine>WFLP</addrLine></address></meeting>
		<imprint>
			<date type="published" when="2011">2011. 2011</date>
			<biblScope unit="volume">6816</biblScope>
			<biblScope unit="page" from="1" to="18" />
		</imprint>
	</monogr>
</biblStruct>

<biblStruct xml:id="b8">
	<analytic>
		<title level="a" type="main">Implementing equational constraints in a functional language</title>
		<author>
			<persName><forename type="first">B</forename><surname>Braßel</surname></persName>
		</author>
		<author>
			<persName><forename type="first">M</forename><surname>Hanus</surname></persName>
		</author>
		<author>
			<persName><forename type="first">B</forename><surname>Peemöller</surname></persName>
		</author>
		<author>
			<persName><forename type="first">F</forename><surname>Reck</surname></persName>
		</author>
	</analytic>
	<monogr>
		<title level="m">Proc. of the 15th International Symposium on Practical Aspects of Declarative Languages (PADL 2013)</title>
				<meeting>of the 15th International Symposium on Practical Aspects of Declarative Languages (PADL 2013)</meeting>
		<imprint>
			<date type="published" when="2013">2013</date>
			<biblScope unit="volume">7752</biblScope>
			<biblScope unit="page" from="125" to="140" />
		</imprint>
	</monogr>
</biblStruct>

<biblStruct xml:id="b9">
	<analytic>
		<title level="a" type="main">A semantics for weakly encapsulated search in functional logic programs</title>
		<author>
			<persName><forename type="first">J</forename><surname>Christiansen</surname></persName>
		</author>
		<author>
			<persName><forename type="first">M</forename><surname>Hanus</surname></persName>
		</author>
		<author>
			<persName><forename type="first">F</forename><surname>Reck</surname></persName>
		</author>
		<author>
			<persName><forename type="first">D</forename><surname>Seidel</surname></persName>
		</author>
	</analytic>
	<monogr>
		<title level="m">Proc. of the 15th International Symposium on Principle and Practice of Declarative Programming (PPDP&apos;13)</title>
				<meeting>of the 15th International Symposium on Principle and Practice of Declarative Programming (PPDP&apos;13)</meeting>
		<imprint>
			<publisher>ACM Press</publisher>
			<date type="published" when="2013">2013</date>
			<biblScope unit="page" from="49" to="60" />
		</imprint>
	</monogr>
</biblStruct>

<biblStruct xml:id="b10">
	<monogr>
		<title level="m" type="main">Prolog -the standard: reference manual</title>
		<author>
			<persName><forename type="first">P</forename><surname>Deransart</surname></persName>
		</author>
		<author>
			<persName><forename type="first">A</forename><surname>Ed-Dbali</surname></persName>
		</author>
		<author>
			<persName><forename type="first">L</forename><surname>Cervoni</surname></persName>
		</author>
		<imprint>
			<date type="published" when="1996">1996</date>
			<publisher>Springer</publisher>
		</imprint>
	</monogr>
</biblStruct>

<biblStruct xml:id="b11">
	<analytic>
		<title level="a" type="main">Termination of rewriting</title>
		<author>
			<persName><forename type="first">N</forename><surname>Dershowitz</surname></persName>
		</author>
	</analytic>
	<monogr>
		<title level="j">J. Symb. Comput</title>
		<imprint>
			<biblScope unit="volume">3</biblScope>
			<biblScope unit="issue">1/2</biblScope>
			<biblScope unit="page" from="69" to="116" />
			<date type="published" when="1987">1987</date>
		</imprint>
	</monogr>
</biblStruct>

<biblStruct xml:id="b12">
	<monogr>
		<title level="m" type="main">A Discipline of Programming</title>
		<author>
			<persName><forename type="first">E</forename><forename type="middle">W</forename><surname>Dijkstra</surname></persName>
		</author>
		<imprint>
			<date type="published" when="1976">1976</date>
			<publisher>Prentice-Hall</publisher>
		</imprint>
	</monogr>
</biblStruct>

<biblStruct xml:id="b13">
	<monogr>
		<title level="m" type="main">The JSON Data Interchange Standard</title>
		<imprint/>
	</monogr>
</biblStruct>

<biblStruct xml:id="b14">
	<monogr>
		<author>
			<persName><forename type="first">M</forename><surname>Hanus</surname></persName>
		</author>
		<author>
			<persName><forename type="first">S</forename><surname>Antoy</surname></persName>
		</author>
		<author>
			<persName><forename type="first">B</forename><surname>Braßel</surname></persName>
		</author>
		<author>
			<persName><forename type="first">M</forename><surname>Engelke</surname></persName>
		</author>
		<author>
			<persName><forename type="first">K</forename><surname>Höppner</surname></persName>
		</author>
		<author>
			<persName><forename type="first">J</forename><surname>Koj</surname></persName>
		</author>
		<author>
			<persName><forename type="first">P</forename><surname>Niederau</surname></persName>
		</author>
		<author>
			<persName><forename type="first">R</forename><surname>Sadre</surname></persName>
		</author>
		<author>
			<persName><forename type="first">F</forename><surname>Steiner</surname></persName>
		</author>
		<ptr target="http://www.informatik.uni-kiel.de/∼pakcs/" />
		<title level="m">PAKCS: The Portland Aachen Kiel Curry System</title>
				<imprint>
			<date type="published" when="2013">2013</date>
		</imprint>
	</monogr>
</biblStruct>

<biblStruct xml:id="b15">
	<monogr>
		<title level="m" type="main">Curry: An integrated functional logic language</title>
		<ptr target="http://www.curry-language.org" />
		<editor>M. Hanus</editor>
		<imprint>
			<date type="published" when="2012">2012</date>
		</imprint>
	</monogr>
	<note>vers. 0.8.3</note>
</biblStruct>

<biblStruct xml:id="b16">
	<analytic>
		<title level="a" type="main">Programming in an integrated functional and logic language</title>
		<author>
			<persName><forename type="first">J</forename><surname>Lloyd</surname></persName>
		</author>
	</analytic>
	<monogr>
		<title level="j">Journal of Functional and Logic Programming</title>
		<imprint>
			<biblScope unit="issue">3</biblScope>
			<biblScope unit="page" from="1" to="49" />
			<date type="published" when="1999">1999. 1999</date>
		</imprint>
	</monogr>
</biblStruct>

<biblStruct xml:id="b17">
	<analytic>
		<title level="a" type="main">A proof theoretic approach to failure in functional logic programming</title>
		<author>
			<persName><forename type="first">F</forename><forename type="middle">J</forename><surname>López-Fraguas</surname></persName>
		</author>
		<author>
			<persName><forename type="first">J</forename><surname>Sánchez-Hernández</surname></persName>
		</author>
	</analytic>
	<monogr>
		<title level="j">Theory and Practice of Logic Programming</title>
		<imprint>
			<biblScope unit="volume">4</biblScope>
			<biblScope unit="issue">1</biblScope>
			<biblScope unit="page" from="41" to="74" />
			<date type="published" when="2004">2004</date>
		</imprint>
	</monogr>
</biblStruct>

<biblStruct xml:id="b18">
	<monogr>
		<title level="m" type="main">Animal Farm: A Fairy Story</title>
		<author>
			<persName><forename type="first">G</forename><surname>Orwell</surname></persName>
		</author>
		<imprint>
			<date type="published" when="1945">1945</date>
			<publisher>Secker and Warburg</publisher>
			<pubPlace>London, UK</pubPlace>
		</imprint>
	</monogr>
</biblStruct>

<biblStruct xml:id="b19">
	<monogr>
		<author>
			<persName><forename type="first">S</forename></persName>
		</author>
		<author>
			<persName><forename type="first">Peyton</forename><surname>Jones</surname></persName>
		</author>
		<title level="m">Haskell 98 Language and Libraries-The Revised Report</title>
				<imprint>
			<publisher>Cambridge University Press</publisher>
			<date type="published" when="2003">2003</date>
		</imprint>
	</monogr>
</biblStruct>

<biblStruct xml:id="b20">
	<analytic>
		<title level="a" type="main">Concurrent Haskell</title>
		<author>
			<persName><forename type="first">S</forename><forename type="middle">L</forename><surname>Peyton Jones</surname></persName>
		</author>
		<author>
			<persName><forename type="first">A</forename><surname>Gordon</surname></persName>
		</author>
		<author>
			<persName><forename type="first">S</forename><surname>Finne</surname></persName>
		</author>
	</analytic>
	<monogr>
		<title level="m">Proc. 23rd ACM Symposium on Principles of Programming Languages (POPL&apos;96)</title>
				<meeting>23rd ACM Symposium on Principles of Programming Languages (POPL&apos;96)</meeting>
		<imprint>
			<publisher>ACM Press</publisher>
			<date type="published" when="1996">1996</date>
			<biblScope unit="page" from="295" to="308" />
		</imprint>
	</monogr>
</biblStruct>

<biblStruct xml:id="b21">
	<analytic>
		<title level="a" type="main">Constructive failure in functional-logic programming: From theory to implementation</title>
		<author>
			<persName><forename type="first">J</forename><surname>Sánchez-Hernández</surname></persName>
		</author>
	</analytic>
	<monogr>
		<title level="j">Journal of Universal Computer Science</title>
		<imprint>
			<biblScope unit="volume">12</biblScope>
			<biblScope unit="issue">11</biblScope>
			<biblScope unit="page" from="1574" to="1593" />
			<date type="published" when="2006">2006</date>
		</imprint>
	</monogr>
</biblStruct>

<biblStruct xml:id="b22">
	<analytic>
		<title level="a" type="main">Automated theorem-proving for theories with simplifiers, commutativity, and associativity</title>
		<author>
			<persName><forename type="first">J</forename><forename type="middle">R</forename><surname>Slagle</surname></persName>
		</author>
	</analytic>
	<monogr>
		<title level="j">Journal of the ACM</title>
		<imprint>
			<biblScope unit="volume">21</biblScope>
			<biblScope unit="issue">4</biblScope>
			<biblScope unit="page" from="622" to="642" />
			<date type="published" when="1974">1974</date>
		</imprint>
	</monogr>
</biblStruct>

				</listBibl>
			</div>
		</back>
	</text>
</TEI>
