20 isort :: "i=>i" |
20 isort :: "i=>i" |
21 qsort :: "i=>i" |
21 qsort :: "i=>i" |
22 |
22 |
23 rules |
23 rules |
24 |
24 |
25 map_def "map(f,l) == lrec(l,[],%x xs g.f(x)$g)" |
25 map_def "map(f,l) == lrec(l,[],%x xs g. f(x)$g)" |
26 comp_def "f o g == (%x.f(g(x)))" |
26 comp_def "f o g == (%x. f(g(x)))" |
27 append_def "l @ m == lrec(l,m,%x xs g.x$g)" |
27 append_def "l @ m == lrec(l,m,%x xs g. x$g)" |
28 mem_def "a mem l == lrec(l,false,%h t g.if eq(a,h) then true else g)" |
28 mem_def "a mem l == lrec(l,false,%h t g. if eq(a,h) then true else g)" |
29 filter_def "filter(f,l) == lrec(l,[],%x xs g.if f`x then x$g else g)" |
29 filter_def "filter(f,l) == lrec(l,[],%x xs g. if f`x then x$g else g)" |
30 flat_def "flat(l) == lrec(l,[],%h t g.h @ g)" |
30 flat_def "flat(l) == lrec(l,[],%h t g. h @ g)" |
31 |
31 |
32 insert_def "insert(f,a,l) == lrec(l,a$[],%h t g.if f`a`h then a$h$t else h$g)" |
32 insert_def "insert(f,a,l) == lrec(l,a$[],%h t g. if f`a`h then a$h$t else h$g)" |
33 isort_def "isort(f) == lam l.lrec(l,[],%h t g.insert(f,h,g))" |
33 isort_def "isort(f) == lam l. lrec(l,[],%h t g. insert(f,h,g))" |
34 |
34 |
35 partition_def |
35 partition_def |
36 "partition(f,l) == letrec part l a b be lcase(l,<a,b>,%x xs. |
36 "partition(f,l) == letrec part l a b be lcase(l,<a,b>,%x xs. |
37 if f`x then part(xs,x$a,b) else part(xs,a,x$b)) |
37 if f`x then part(xs,x$a,b) else part(xs,a,x$b)) |
38 in part(l,[],[])" |
38 in part(l,[],[])" |
39 qsort_def "qsort(f) == lam l. letrec qsortx l be lcase(l,[],%h t. |
39 qsort_def "qsort(f) == lam l. letrec qsortx l be lcase(l,[],%h t. |
40 let p be partition(f`h,t) |
40 let p be partition(f`h,t) |
41 in split(p,%x y.qsortx(x) @ h$qsortx(y))) |
41 in split(p,%x y. qsortx(x) @ h$qsortx(y))) |
42 in qsortx(l)" |
42 in qsortx(l)" |
43 |
43 |
44 end |
44 end |