Implement the "contains a free variable named _j_" example.
Chris Pressey
3 years ago
| 181 | 181 |
### Example 1
|
| 182 | 182 |
|
| 183 | 183 |
As a warm-up, suppose we want to write a function that tells us if a
|
| 184 | |
lambda term contains any free variable named `j`.
|
|
184 |
lambda term contains any free variable named (for the sake of
|
|
185 |
concreteness, let's say) `j`.
|
| 185 | 186 |
|
| 186 | 187 |
In this implementation and those that follow, we will assume we have
|
| 187 | 188 |
a simple functional language with the usual accoutrements (recursion,
|
|
| 195 | 196 |
of names that we don't want it to return. In this particular case,
|
| 196 | 197 |
that set is the singleton set containing only `j`.
|
| 197 | 198 |
|
| 198 | |
--
|
| 199 | |
-- UNTESTED
|
| 200 | |
--
|
| 201 | 199 |
let contains_j = fun(t, ns) ->
|
| 202 | 200 |
destruct(r,
|
| 203 | 201 |
fun(n) -> n == "j",
|
| 204 | |
fun(t, u) -> contains_j(t) || contains_j(u),
|
|
202 |
fun(t, u) -> contains_j(t, ns) || contains_j(u, ns),
|
| 205 | 203 |
fun(t) ->
|
| 206 | 204 |
let
|
| 207 | 205 |
(n, ns') = pick(ns, ~{"j"})
|
| 208 | 206 |
t' = resolve(t, var(n))
|
| 209 | 207 |
in
|
| 210 | |
contains_j(t')
|
|
208 |
contains_j(t', ns')
|
| 211 | 209 |
)
|
| 212 | 210 |
|
| 213 | 211 |
### Example 2
|
| 47 | 47 |
excluded = elem n exclude
|
| 48 | 48 |
in
|
| 49 | 49 |
if excluded then pick exclude names' else (n, names')
|
|
50 |
|
|
51 |
--
|
|
52 |
-- "Contains a free variable named _j_" example
|
|
53 |
--
|
|
54 |
|
|
55 |
contains j t names =
|
|
56 |
destruct t
|
|
57 |
(\n -> n == j)
|
|
58 |
(\u v -> contains j u names || contains j v names)
|
|
59 |
(\u ->
|
|
60 |
let
|
|
61 |
(n, names') = pick [j] names
|
|
62 |
t' = resolve t (var n)
|
|
63 |
in
|
|
64 |
contains j t' names'
|
|
65 |
)
|
|
66 |
|
|
67 |
testContains1 = contains "n" test1 names -- True
|
|
68 |
testContains2 = contains "m" test1 names -- False
|
|
69 |
testContains3 = contains "n" (abs "n" (var "n")) names -- False
|