moved applications to separate page
[lambda.git] / week2.mdwn
1 1.      Substitution; using alpha-conversion and other strategies
2 1.      Conversion versus reduction
3
4 1.      Different evaluation strategies (call by name, call by value, etc.)
5 1.      Strongly normalizing vs weakly normalizing vs non-normalizing; Church-Rosser Theorem(s)
6 1.      Lambda calculus compared to combinatorial logic<p>
7 1.      Church-like encodings of numbers, defining addition and multiplication
8 1.      Defining the predecessor function; alternate encodings for the numbers
9 1.      Homogeneous sequences or "lists"; how they differ from pairs, triples, etc.
10 1.      Representing lists as pairs
11 1.      Representing lists as folds
12 1.      Typical higher-order functions: map, filter, fold<p>
13 1.      Recursion exploiting the fold-like representation of numbers and lists ([[!wikipedia Deforestation (computer science)]], [[!wikipedia Zipper (data structure)]])
14 1.      General recursion using omega
15
16 1.      Eta reduction and "extensionality" ??
17 Undecidability of equivalence
18
19 There is no algorithm which takes as input two lambda expressions and outputs TRUE or FALSE depending on whether or not the two expressions are equivalent. This was historically the first problem for which undecidability could be proven. As is common for a proof of undecidability, the proof shows that no computable function can decide the equivalence. Church's thesis is then invoked to show that no algorithm can do so.
20
21 Church's proof first reduces the problem to determining whether a given lambda expression has a normal form. A normal form is an equivalent expression which cannot be reduced any further under the rules imposed by the form. Then he assumes that this predicate is computable, and can hence be expressed in lambda calculus. Building on earlier work by Kleene and constructing a Gödel numbering for lambda expressions, he constructs a lambda expression e which closely follows the proof of Gödel's first incompleteness theorem. If e is applied to its own Gödel number, a contradiction results.
22
23
24
25 1.      The Y combinator(s); more on evaluation strategies<p>
26 1.      Introducing the notion of a "continuation", which technique we'll now already have used a few times
27
28
29
30 alpha-convertible
31
32 syntactic equality `===`
33 contract/reduce/`~~>`
34 convertible `<~~>`
35
36 normalizing
37         weakly normalizable
38         strongly normalizable
39         "normal order" reduction vs "applicative order"
40         eval strategy choices
41
42                                 Reduction strategies For more details on this topic, see Evaluation
43                 strategy.
44
45                                 Whether a term is normalising or not, and how much work needs to be
46                 done in normalising it if it is, depends to a large extent on the reduction
47                 strategy used. The distinction between reduction strategies relates to the
48                 distinction in functional programming languages between eager evaluation and
49                 lazy evaluation.
50
51                                 Full beta reductions Any redex can be reduced at any time. This means
52                 essentially the lack of any particular reduction strategy—with regard to
53                 reducibility, "all bets are off". Applicative order The leftmost, innermost
54                 redex is always reduced first. Intuitively this means a function's arguments
55                 are always reduced before the function itself. Applicative order always
56                 attempts to apply functions to normal forms, even when this is not possible.
57                 Most programming languages (including Lisp, ML and imperative languages like C
58                 and Java) are described as "strict", meaning that functions applied to
59                 non-normalising arguments are non-normalising. This is done essentially using
60                 applicative order, call by value reduction (see below), but usually called
61                 "eager evaluation". Normal order The leftmost, outermost redex is always
62                 reduced first. That is, whenever possible the arguments are substituted into
63                 the body of an abstraction before the arguments are reduced. Call by name As
64                 normal order, but no reductions are performed inside abstractions. For example
65                 λx.(λx.x)x is in normal form according to this strategy, although it contains
66                 the redex (λx.x)x. Call by value Only the outermost redexes are reduced: a
67                 redex is reduced only when its right hand side has reduced to a value (variable
68                 or lambda abstraction). Call by need As normal order, but function applications
69                 that would duplicate terms instead name the argument, which is then reduced
70                 only "when it is needed". Called in practical contexts "lazy evaluation". In
71                 implementations this "name" takes the form of a pointer, with the redex
72                 represented by a thunk.
73
74                                 Applicative order is not a normalising strategy. The usual
75                 counterexample is as follows: define Ω = ωω where ω = λx.xx. This entire
76                 expression contains only one redex, namely the whole expression; its reduct is
77                 again Ω. Since this is the only available reduction, Ω has no normal form
78                 (under any evaluation strategy). Using applicative order, the expression KIΩ =
79                 (λxy.x) (λx.x)Ω is reduced by first reducing Ω to normal form (since it is the
80                 leftmost redex), but since Ω has no normal form, applicative order fails to
81                 find a normal form for KIΩ.
82
83                                 In contrast, normal order is so called because it always finds a
84                 normalising reduction if one exists. In the above example, KIΩ reduces under
85                 normal order to I, a normal form. A drawback is that redexes in the arguments
86                 may be copied, resulting in duplicated computation (for example, (λx.xx)
87                 ((λx.x)y) reduces to ((λx.x)y) ((λx.x)y) using this strategy; now there are two
88                 redexes, so full evaluation needs two more steps, but if the argument had been
89                 reduced first, there would now be none).
90
91                                 The positive tradeoff of using applicative order is that it does not
92                 cause unnecessary computation if all arguments are used, because it never
93                 substitutes arguments containing redexes and hence never needs to copy them
94                 (which would duplicate work). In the above example, in applicative order
95                 (λx.xx) ((λx.x)y) reduces first to (λx.xx)y and then to the normal order yy,
96                 taking two steps instead of three.
97
98                                 Most purely functional programming languages (notably Miranda and its
99                 descendents, including Haskell), and the proof languages of theorem provers,
100                 use lazy evaluation, which is essentially the same as call by need. This is
101                 like normal order reduction, but call by need manages to avoid the duplication
102                 of work inherent in normal order reduction using sharing. In the example given
103                 above, (λx.xx) ((λx.x)y) reduces to ((λx.x)y) ((λx.x)y), which has two redexes,
104                 but in call by need they are represented using the same object rather than
105                 copied, so when one is reduced the other is too.
106
107
108
109
110                 Strict evaluation Main article: strict evaluation
111
112                 In strict evaluation, the arguments to a function are always evaluated
113                 completely before the function is applied.
114
115                 Under Church encoding, eager evaluation of operators maps to strict evaluation
116                 of functions; for this reason, strict evaluation is sometimes called "eager".
117                 Most existing programming languages use strict evaluation for functions. [edit]
118                 Applicative order
119
120                 Applicative order (or leftmost innermost) evaluation refers to an evaluation
121                 strategy in which the arguments of a function are evaluated from left to right
122                 in a post-order traversal of reducible expressions (redexes). Unlike
123                 call-by-value, applicative order evaluation reduces terms within a function
124                 body as much as possible before the function is applied. [edit] Call by value
125
126                 Call-by-value evaluation (also referred to as pass-by-value) is the most common
127                 evaluation strategy, used in languages as different as C and Scheme. In
128                 call-by-value, the argument expression is evaluated, and the resulting value is
129                 bound to the corresponding variable in the function (frequently by copying the
130                 value into a new memory region). If the function or procedure is able to assign
131                 values to its parameters, only its local copy is assigned — that is, anything
132                 passed into a function call is unchanged in the caller's scope when the
133                 function returns.
134
135                 Call-by-value is not a single evaluation strategy, but rather the family of
136                 evaluation strategies in which a function's argument is evaluated before being
137                 passed to the function. While many programming languages (such as Eiffel and
138                 Java) that use call-by-value evaluate function arguments left-to-right, some
139                 evaluate functions and their arguments right-to-left, and others (such as
140                 Scheme, OCaml and C) leave the order unspecified (though they generally require
141                 implementations to be consistent).
142
143                 In some cases, the term "call-by-value" is problematic, as the value which is
144                 passed is not the value of the variable as understood by the ordinary meaning
145                 of value, but an implementation-specific reference to the value. The
146                 description "call-by-value where the value is a reference" is common (but
147                 should not be understood as being call-by-reference); another term is
148                 call-by-sharing. Thus the behaviour of call-by-value Java or Visual Basic and
149                 call-by-value C or Pascal are significantly different: in C or Pascal, calling
150                 a function with a large structure as an argument will cause the entire
151                 structure to be copied, potentially causing serious performance degradation,
152                 and mutations to the structure are invisible to the caller. However, in Java or
153                 Visual Basic only the reference to the structure is copied, which is fast, and
154                 mutations to the structure are visible to the caller. [edit] Call by reference
155
156                 In call-by-reference evaluation (also referred to as pass-by-reference), a
157                 function receives an implicit reference to the argument, rather than a copy of
158                 its value. This typically means that the function can modify the argument-
159                 something that will be seen by its caller. Call-by-reference therefore has the
160                 advantage of greater time- and space-efficiency (since arguments do not need to
161                 be copied), as well as the potential for greater communication between a
162                 function and its caller (since the function can return information using its
163                 reference arguments), but the disadvantage that a function must often take
164                 special steps to "protect" values it wishes to pass to other functions.
165
166                 Many languages support call-by-reference in some form or another, but
167                 comparatively few use it as a default; Perl and Visual Basic are two that do,
168                 though Visual Basic also offers a special syntax for call-by-value parameters.
169                 A few languages, such as C++ and REALbasic, default to call-by-value, but offer
170                 special syntax for call-by-reference parameters. C++ additionally offers
171                 call-by-reference-to-const. In purely functional languages there is typically
172                 no semantic difference between the two strategies (since their data structures
173                 are immutable, so there is no possibility for a function to modify any of its
174                 arguments), so they are typically described as call-by-value even though
175                 implementations frequently use call-by-reference internally for the efficiency
176                 benefits.
177
178                 Even among languages that don't exactly support call-by-reference, many,
179                 including C and ML, support explicit references (objects that refer to other
180                 objects), such as pointers (objects representing the memory addresses of other
181                 objects), and these can be used to effect or simulate call-by-reference (but
182                 with the complication that a function's caller must explicitly generate the
183                 reference to supply as an argument). [edit] Call by sharing
184
185                 Also known as "call by object" or "call by object-sharing" is an evaluation
186                 strategy first named by Barbara Liskov et al. for the language CLU in 1974[1].
187                 It is used by languages such as Python[2], Iota, Java (for object
188                 references)[3], Ruby, Scheme, OCaml, AppleScript, and many other languages.
189                 However, the term "call by sharing" is not in common use; the terminology is
190                 inconsistent across different sources. For example, in the Java community, they
191                 say that Java is pass-by-value, whereas in the Ruby community, they say that
192                 Ruby is pass-by-reference, even though the two languages exhibit the same
193                 semantics. Call-by-sharing implies that values in the language are based on
194                 objects rather than primitive types.
195
196                 The semantics of call-by-sharing differ from call-by-reference in that
197                 assignments to function arguments within the function aren't visible to the
198                 caller (unlike by-reference semantics)[citation needed]. However since the
199                 function has access to the same object as the caller (no copy is made),
200                 mutations to those objects within the function are visible to the caller, which
201                 differs from call-by-value semantics.
202
203                 Although this term has widespread usage in the Python community, identical
204                 semantics in other languages such as Java and Visual Basic are often described
205                 as call-by-value, where the value is implied to be a reference to the object.
206                 [edit] Call by copy-restore
207
208                 Call-by-copy-restore, call-by-value-result or call-by-value-return (as termed
209                 in the Fortran community) is a special case of call-by-reference where the
210                 provided reference is unique to the caller. If a parameter to a function call
211                 is a reference that might be accessible by another thread of execution, its
212                 contents are copied to a new reference that is not; when the function call
213                 returns, the updated contents of this new reference are copied back to the
214                 original reference ("restored").
215
216                 The semantics of call-by-copy-restore also differ from those of
217                 call-by-reference where two or more function arguments alias one another; that
218                 is, point to the same variable in the caller's environment. Under
219                 call-by-reference, writing to one will affect the other; call-by-copy-restore
220                 avoids this by giving the function distinct copies, but leaves the result in
221                 the caller's environment undefined (depending on which of the aliased arguments
222                 is copied back first).
223
224                 When the reference is passed to the callee uninitialized, this evaluation
225                 strategy may be called call-by-result. [edit] Partial evaluation Main article:
226                 Partial evaluation
227
228                 In partial evaluation, evaluation may continue into the body of a function that
229                 has not been applied. Any sub-expressions that do not contain unbound variables
230                 are evaluated, and function applications whose argument values are known may be
231                 reduced. In the presence of side-effects, complete partial evaluation may
232                 produce unintended results; for this reason, systems that support partial
233                 evaluation tend to do so only for "pure" expressions (expressions without
234                 side-effects) within functions. [edit] Non-strict evaluation
235
236                 In non-strict evaluation, arguments to a function are not evaluated unless they
237                 are actually used in the evaluation of the function body.
238
239                 Under Church encoding, lazy evaluation of operators maps to non-strict
240                 evaluation of functions; for this reason, non-strict evaluation is often
241                 referred to as "lazy". Boolean expressions in many languages use lazy
242                 evaluation; in this context it is often called short circuiting. Conditional
243                 expressions also usually use lazy evaluation, albeit for different reasons.
244                 [edit] Normal order
245
246                 Normal-order (or leftmost outermost) evaluation is the evaluation strategy
247                 where the outermost redex is always reduced, applying functions before
248                 evaluating function arguments. It differs from call-by-name in that
249                 call-by-name does not evaluate inside the body of an unapplied
250                 function[clarification needed]. [edit] Call by name
251
252                 In call-by-name evaluation, the arguments to functions are not evaluated at all
253                 — rather, function arguments are substituted directly into the function body
254                 using capture-avoiding substitution. If the argument is not used in the
255                 evaluation of the function, it is never evaluated; if the argument is used
256                 several times, it is re-evaluated each time. (See Jensen's Device.)
257
258                 Call-by-name evaluation can be preferable over call-by-value evaluation because
259                 call-by-name evaluation always yields a value when a value exists, whereas
260                 call-by-value may not terminate if the function's argument is a non-terminating
261                 computation that is not needed to evaluate the function. Opponents of
262                 call-by-name claim that it is significantly slower when the function argument
263                 is used, and that in practice this is almost always the case as a mechanism
264                 such as a thunk is needed. [edit] Call by need
265
266                 Call-by-need is a memoized version of call-by-name where, if the function
267                 argument is evaluated, that value is stored for subsequent uses. In a "pure"
268                 (effect-free) setting, this produces the same results as call-by-name; when the
269                 function argument is used two or more times, call-by-need is almost always
270                 faster.
271
272                 Because evaluation of expressions may happen arbitrarily far into a
273                 computation, languages using call-by-need generally do not support
274                 computational effects (such as mutation) except through the use of monads and
275                 uniqueness types. This eliminates any unexpected behavior from variables whose
276                 values change prior to their delayed evaluation.
277
278                 This is a kind of Lazy evaluation.
279
280                 Haskell is the most well-known language that uses call-by-need evaluation.
281
282                 R also uses a form of call-by-need. [edit] Call by macro expansion
283
284                 Call-by-macro-expansion is similar to call-by-name, but uses textual
285                 substitution rather than capture-avoiding substitution. With uncautious use,
286                 macro substitution may result in variable capture and lead to undesired
287                 behavior. Hygienic macros avoid this problem by checking for and replacing
288                 shadowed variables that are not parameters.
289
290
291
292
293                 Eager evaluation or greedy evaluation is the evaluation strategy in most
294                 traditional programming languages.
295
296                 In eager evaluation an expression is evaluated as soon as it gets bound to a
297                 variable. The term is typically used to contrast lazy evaluation, where
298                 expressions are only evaluated when evaluating a dependent expression. Eager
299                 evaluation is almost exclusively used in imperative programming languages where
300                 the order of execution is implicitly defined by the source code organization.
301
302                 One advantage of eager evaluation is that it eliminates the need to track and
303                 schedule the evaluation of expressions. It also allows the programmer to
304                 dictate the order of execution, making it easier to determine when
305                 sub-expressions (including functions) within the expression will be evaluated,
306                 as these sub-expressions may have side-effects that will affect the evaluation
307                 of other expressions.
308
309                 A disadvantage of eager evaluation is that it forces the evaluation of
310                 expressions that may not be necessary at run time, or it may delay the
311                 evaluation of expressions that have a more immediate need. It also forces the
312                 programmer to organize the source code for optimal order of execution.
313
314                 Note that many modern compilers are capable of scheduling execution to better
315                 optimize processor resources and can often eliminate unnecessary expressions
316                 from being executed entirely. Therefore, the notions of purely eager or purely
317                 lazy evaluation may not be applicable in practice.
318
319
320
321                 In computer programming, lazy evaluation is the technique of delaying a
322                 computation until the result is required.
323
324                 The benefits of lazy evaluation include: performance increases due to avoiding
325                 unnecessary calculations, avoiding error conditions in the evaluation of
326                 compound expressions, the capability of constructing potentially infinite data
327                 structures, and the capability of defining control structures as abstractions
328                 instead of as primitives.
329
330                 Languages that use lazy actions can be further subdivided into those that use a
331                 call-by-name evaluation strategy and those that use call-by-need. Most
332                 realistic lazy languages, such as Haskell, use call-by-need for performance
333                 reasons, but theoretical presentations of lazy evaluation often use
334                 call-by-name for simplicity.
335
336                 The opposite of lazy actions is eager evaluation, sometimes known as strict
337                 evaluation. Eager evaluation is the evaluation behavior used in most
338                 programming languages.
339
340                 Lazy evaluation refers to how expressions are evaluated when they are passed as
341                 arguments to functions and entails the following three points:[1]
342
343                    1. The expression is only evaluated if the result is required by the calling
344                 function, called delayed evaluation.[2] 2. The expression is only evaluated to
345                 the extent that is required by the calling function, called short-circuit
346                 evaluation. 3. The expression is never evaluated more than once, called
347                 applicative-order evaluation.[3]
348
349                 Contents [hide]
350
351                         * 1 Delayed evaluation
352                                   o 1.1 Control structures
353                         * 2 Controlling eagerness in lazy languages 3 Other uses 4 See also 5
354                         * References 6 External links
355
356                 [edit] Delayed evaluation
357
358                 Delayed evaluation is used particularly in functional languages. When using
359                 delayed evaluation, an expression is not evaluated as soon as it gets bound to
360                 a variable, but when the evaluator is forced to produce the expression's value.
361                 That is, a statement such as x:=expression; (i.e. the assignment of the result
362                 of an expression to a variable) clearly calls for the expression to be
363                 evaluated and the result placed in x, but what actually is in x is irrelevant
364                 until there is a need for its value via a reference to x in some later
365                 expression whose evaluation could itself be deferred, though eventually the
366                 rapidly-growing tree of dependencies would be pruned in order to produce some
367                 symbol rather than another for the outside world to see.
368
369                 Some programming languages delay evaluation of expressions by default, and some
370                 others provide functions or special syntax to delay evaluation. In Miranda and
371                 Haskell, evaluation of function arguments is delayed by default. In many other
372                 languages, evaluation can be delayed by explicitly suspending the computation
373                 using special syntax (as with Scheme's "delay" and "force" and OCaml's "lazy"
374                 and "Lazy.force") or, more generally, by wrapping the expression in a thunk.
375                 The object representing such an explicitly delayed evaluation is called a
376                 future or promise. Perl 6 uses lazy evaluation of lists, so one can assign
377                 infinite lists to variables and use them as arguments to functions, but unlike
378                 Haskell and Miranda, Perl 6 doesn't use lazy evaluation of arithmetic operators
379                 and functions by default.
380
381                 Delayed evaluation has the advantage of being able to create calculable
382                 infinite lists without infinite loops or size matters interfering in
383                 computation. For example, one could create a function that creates an infinite
384                 list (often called a stream) of Fibonacci numbers. The calculation of the n-th
385                 Fibonacci number would be merely the extraction of that element from the
386                 infinite list, forcing the evaluation of only the first n members of the list.
387
388                 For example, in Haskell, the list of all Fibonacci numbers can be written as
389
390                  fibs = 0 : 1 : zipWith (+) fibs (tail fibs)
391
392                 In Haskell syntax, ":" prepends an element to a list, tail returns a list
393                 without its first element, and zipWith uses a specified function (in this case
394                 addition) to combine corresponding elements of two lists to produce a third.
395
396                 Provided the programmer is careful, only the values that are required to
397                 produce a particular result are evaluated. However, certain calculations may
398                 result in the program attempting to evaluate an infinite number of elements;
399                 for example, requesting the length of the list or trying to sum the elements of
400                 the list with a fold operation would result in the program either failing to
401                 terminate or running out of memory. [edit] Control structures
402
403                 Even in most eager languages if statements evaluate in a lazy fashion.
404
405                 if a then b else c
406
407                 evaluates (a), then if and only if (a) evaluates to true does it evaluate (b),
408                 otherwise it evaluates (c). That is, either (b) or (c) will not be evaluated.
409                 Conversely, in an eager language the expected behavior is that
410
411                 define f(x,y) = 2*x set k = f(e,5)
412
413                 will still evaluate (e) and (f) when computing (k). However, user-defined
414                 control structures depend on exact syntax, so for example
415
416                 define g(a,b,c) = if a then b else c l = g(h,i,j)
417
418                 (i) and (j) would both be evaluated in an eager language. While in
419
420                 l' = if h then i else j
421
422                 (i) or (j) would be evaluated, but never both.
423
424                 Lazy evaluation allows control structures to be defined normally, and not as
425                 primitives or compile-time techniques. If (i) or (j) have side effects or
426                 introduce run time errors, the subtle differences between (l) and (l') can be
427                 complex. As most programming languages are Turing-complete, it is of course
428                 possible to introduce lazy control structures in eager languages, either as
429                 built-ins like C's ternary operator ?: or by other techniques such as clever
430                 use of lambdas, or macros.
431
432                 Short-circuit evaluation of Boolean control structures is sometimes called
433                 "lazy". [edit] Controlling eagerness in lazy languages
434
435                 In lazy programming languages such as Haskell, although the default is to
436                 evaluate expressions only when they are demanded, it is possible in some cases
437                 to make code more eager—or conversely, to make it more lazy again after it has
438                 been made more eager. This can be done by explicitly coding something which
439                 forces evaluation (which may make the code more eager) or avoiding such code
440                 (which may make the code more lazy). Strict evaluation usually implies
441                 eagerness, but they are technically different concepts.
442
443                 However, there is an optimisation implemented in some compilers called
444                 strictness analysis, which, in some cases, allows the compiler to infer that a
445                 value will always be used. In such cases, this may render the programmer's
446                 choice of whether to force that particular value or not, irrelevant, because
447                 strictness analysis will force strict evaluation.
448
449                 In Haskell, marking constructor fields strict means that their values will
450                 always be demanded immediately. The seq function can also be used to demand a
451                 value immediately and then pass it on, which is useful if a constructor field
452                 should generally be lazy. However, neither of these techniques implements
453                 recursive strictness—for that, a function called deepSeq was invented.
454
455                 Also, pattern matching in Haskell 98 is strict by default, so the ~ qualifier
456                 has to be used to make it lazy. [edit] 
457
458
459
460
461 confluence/Church-Rosser
462
463
464 "combinators", useful ones:
465
466 Useful combinators
467 I
468 K
469 omega
470 true/get-first/K
471 false/get-second
472 make-pair
473 S,B,C,W/dup,Omega
474
475 (( combinatorial logic ))
476
477 composition
478 n-ary[sic] composition
479 "fold-based"[sic] representation of numbers
480 defining some operations, not yet predecessor
481         iszero,succ,add,mul,...?
482
483 lists?
484         explain differences between list and tuple (and stream)
485                 FIFO queue,LIFO stack,etc...
486 "pair-based" representation of lists (1,2,3)
487 nil,cons,isnil,head,tail
488
489 explain operations like "map","filter","fold_left","fold_right","length","reverse"
490 but we're not yet in position to implement them because we don't know how to recurse
491
492 Another way to do lists is based on model of how we did numbers
493 "fold-based" representation of lists
494 One virtue is we can do some recursion by exploiting the fold-based structure of our implementation; don't (yet) need a general method for recursion
495
496 Go back to numbers, how to do predecessor? (a few ways)
497 For some purposes may be easier (to program,more efficient) to use "pair-based" representation of numbers
498 ("More efficient" but these are still base-1 representations of numbers!)
499 In this case, too you'd need a general method for recursion
500 (You could also have a hybrid, pair-and-fold based representation of numbers, and a hybrid, pair-and-fold based representation of lists. Works quite well.)
501
502 Recursion
503 Even if we have fold-based representation of numbers, and predecessor/equal/subtraction, some recursive functions are going to be out of our reach
504 Need a general method, where f(n) doesn't just depend on f(n-1) (or <f(n-1),f(n-2),...>). Example?
505
506 How to do with recursion with omega.
507
508
509 Next week: fixed point combinators
510
511