LCME Воскресенье, 28.05.2017, 04:03
Главная | Регистрация | Вход Приветствую Вас Гость | RSS
[ Новые сообщения · Участники · Правила форума · Поиск · RSS ]
Страница 1 из 11
Модератор форума: anatoliy 
Форум » Домашние задания » Программирование » Домашнее задание от 06.10 (Перевод в SK)
Домашнее задание от 06.10
freidomДата: Четверг, 08.10.2009, 00:29 | Сообщение # 1
Главный тут
Группа: Администраторы
Сообщений: 273
Репутация: 20
Статус: 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)));

Прикрепления: 6975120.ml(7Kb)
 
Форум » Домашние задания » Программирование » Домашнее задание от 06.10 (Перевод в SK)
Страница 1 из 11
Поиск:

Copyright Freidom © 2017 Хостинг от uCoz