moved applications to separate page
[lambda.git] / lists.mdwn
1 (list?)
2 nil
3 cons
4 nil?, (pair?)
5 head
6 tail
7
8 Chris's lists:
9         nil = (t,N)  = \f. f true N
10         [a] = (f,(a,nil))
11         [b,a] = (f,(b,[a]))
12
13 isnil = get-first
14 head = L get-second get-first
15 tail = L get-second get-second
16
17 would be nice if nil tail = nil
18         nil tail = (t, N) get-second get-second = N get-second
19         so N get-second should be (t,N)
20         e.g. N = K (t,N)
21                    = (\n. K (t,n)) N
22         How to do that?
23         a fixed point g_ of g : g_ = (g g_)
24         (Y g) = g (Y g)
25         N = (\n. K (t,n)) N is of the form N = g N
26         So if we just set N = Y g, we'll have what we want. N = (Y g) = g (Y g) = g N
27         
28         i.e. N = Y g = Y (\n. K (t,n))
29         and nil = (t, N) = (t, Y (\n. K (t, n)))
30
31         nil get-second get-second ~~>
32                 Y (\n. K (t, n)) get-second     ~~>
33                 (\n. K (t, n)) (Y (\n. K (t,n))) get-second ~~>
34                 K (t, Y (\n. K (t,n))) get-second ~~>
35                 (t, Y (\n. K (t,n)))
36
37
38 Lists 2:
39         nil = false
40         [a] = (a,nil)
41
42 L (\h\t.K deal_with_h_and_t) if-nil
43
44 We've already seen enumerations: true | false, red | green | blue
45 What if you want one or more of the elements to have associated data? e.g. red | green | blue <how-blue>
46
47 could handle like this:
48         the-value if-red if-green (\n. handler-if-blue-to-degree-n)
49
50         then red = \r \g \b-handler. r
51                  green = \r \g \b-handler. g
52                  make-blue = \degree. \r \g \b-handler. b-handler degree
53
54 A list is basically: empty | non-empty <head,tail>
55
56                 empty = \non-empty-handler \if-empty. if-empty = false
57                 cons = \h \t. \non-empty-handler \if-empty. non-empty-handler h t
58
59                 so [a] = cons a empty = \non-empty-handler \_. non-empty-handler a empty
60
61
62
63 Lists 3:
64 [a; tl] isnil == (\f. f a tl) (\h \t.false) a b ~~> false a b
65
66 nil isnil == (\f. M) (\h \t. false) a b ~~> M[f:=isnil] a b == a
67
68         so M could be \a \b. a, i.e. true
69         so nil = \f. true == K true == K K = \_ K
70
71         nil = K true
72         [a] = (a,nil)
73         [b,a] = (b,[a])
74
75 isnil = (\x\y.false)
76
77 nil tail = K true tail = true = \x\y.x = \f.f? such that f? = Kx. there is no such.
78 nil head = K true head = true. could mislead.
79
80