+++ /dev/null
-(list?)
-nil
-cons
-nil?, (pair?)
-head
-tail
-
-Chris's lists:
- nil = (t,N) = \f. f true N
- [a] = (f,(a,nil))
- [b,a] = (f,(b,[a]))
-
-isnil = get-first
-head = L get-second get-first
-tail = L get-second get-second
-
-would be nice if nil tail = nil
- nil tail = (t, N) get-second get-second = N get-second
- so N get-second should be (t,N)
- e.g. N = K (t,N)
- = (\n. K (t,n)) N
- How to do that?
- a fixed point g_ of g : g_ = (g g_)
- (Y g) = g (Y g)
- N = (\n. K (t,n)) N is of the form N = g N
- So if we just set N = Y g, we'll have what we want. N = (Y g) = g (Y g) = g N
-
- i.e. N = Y g = Y (\n. K (t,n))
- and nil = (t, N) = (t, Y (\n. K (t, n)))
-
- nil get-second get-second ~~>
- Y (\n. K (t, n)) get-second ~~>
- (\n. K (t, n)) (Y (\n. K (t,n))) get-second ~~>
- K (t, Y (\n. K (t,n))) get-second ~~>
- (t, Y (\n. K (t,n)))
-
-
-Lists 2:
- nil = false
- [a] = (a,nil)
-
-L (\h\t.K deal_with_h_and_t) if-nil
-
-We've already seen enumerations: true | false, red | green | blue
-What if you want one or more of the elements to have associated data? e.g. red | green | blue <how-blue>
-
-could handle like this:
- the-value if-red if-green (\n. handler-if-blue-to-degree-n)
-
- then red = \r \g \b-handler. r
- green = \r \g \b-handler. g
- make-blue = \degree. \r \g \b-handler. b-handler degree
-
-A list is basically: empty | non-empty <head,tail>
-
- empty = \non-empty-handler \if-empty. if-empty = false
- cons = \h \t. \non-empty-handler \if-empty. non-empty-handler h t
-
- so [a] = cons a empty = \non-empty-handler \_. non-empty-handler a empty
-
-
-
-Lists 3:
-[a; tl] isnil == (\f. f a tl) (\h \t.false) a b ~~> false a b
-
-nil isnil == (\f. M) (\h \t. false) a b ~~> M[f:=isnil] a b == a
-
- so M could be \a \b. a, i.e. true
- so nil = \f. true == K true == K K = \_ K
-
- nil = K true
- [a] = (a,nil)
- [b,a] = (b,[a])
-
-isnil = (\x\y.false)
-
-nil tail = K true tail = true = \x\y.x = \f.f? such that f? = Kx. there is no such.
-nil head = K true head = true. could mislead.
-
-