| freidom | Дата: Четверг, 08.10.2009, 00:29 | Сообщение # 1 |
 Главный тут
Группа: Администраторы
Сообщений: 273
Статус: Offline
| Короче, на этот раз всё плохо...
Погуглил и напоролся на википедийскую статью http://en.wikipedia.org/wiki/Combinatory_logic , где есть несколько слов про SK. А точнее: Quote It is a perhaps astonishing fact that S and K can be composed to produce combinators that are extensionally equal to any lambda term, and therefore, by Church's thesis, to any computable function whatsoever. The proof is to present a transformation, T[ ], which converts an arbitrary lambda term into an equivalent combinator. T[ ] may be defined as follows:
T[x] => x
T[(E₁ E₂)] => (T[E₁] T[E₂])
T[λx.E] => (K T[E]) (if x is not free in E)
T[λx.x] => I
T[λx.λy.E] => T[λx.T[λy.E]] (if x is free in E)
T[λx.(E₁ E₂)] => (S T[λx.E₁] T[λx.E₂]) This process is also known as abstraction elimination. Ну, автоматически напрашивается ML-ный эквивалент: Code let rec sk z =
match z with
Var b -> Var b
|Abs (x, Abs (y, Abs (z, App (App (Var a, Var c), App (Var b, Var d))))) when a = x && b = y && c = z && c = d -> s
|Abs (x, Abs (y, Var z)) when x = z -> k
|Abs (x, Var y) when x = y -> i
|App (p, q) -> App (sk p, sk q)
|Abs (x, q) when not (isin (fv q) x) -> App (k, sk q)
|Abs (x, Abs (y, q)) when isin (fv q) x -> sk (Abs (x, sk (Abs (y, q))))
|Abs (x, App (p, q)) -> App (App (s, sk p), sk q)
|_ -> Nil;; Где Code let s = Abs ("x", Abs ("y", Abs ("z", App (App (Var "x", Var "z"), App (Var "y", Var "z")))));;
let k = Abs ("x", Abs ("y", Var "x"));;
let i = Abs ("x", Var "x");; К сожалению, функция выдаёт полный бред: \xyz.y(xyz) -> (SSSy)(xyz), что нехорошо. Ну а по type sk = S of sk list | K of sk list;; у меня идей вообще нету. (читай: WTF?!) P.S.: я идиот...
Quote Все дело в предпоследнем случае (это же вылезало и на уроке тоже): |Abs (x, App (p, q)) -> App (App (s, sk p), sk q) Ты не втаскиваешь абстракцию внутрь применения. Правильно так: |Abs (x, App (p, q)) -> App (App (s, sk (Abs (x, p))), sk (Abs (x, q))); |
| |
| |
