LCME Пятница, 04.10.2024, 08:11
Главная | Регистрация | Вход Приветствую Вас Гость | RSS
[ Новые сообщения · Участники · Правила форума · Поиск · RSS ]
  • Страница 1 из 1
  • 1
Модератор форума: anatoliy  
Классная работа от 06.10
freidomДата: Вторник, 06.10.2009, 13:49 | Сообщение # 1
Главный тут
Группа: Администраторы
Сообщений: 273
Репутация: 20
Статус: Offline
open List;;
type lambda = Var of string
| App of (lambda * lambda)
| Abs of (string * lambda)
| Nil;;

let y_term = Abs ("f", App (Abs ("x", App (Var ("f"), (App (Var ("x"), Var ("x"))))),
Abs ("x", App (Var ("f"), (App (Var ("x"), Var ("x")))))));;

let xred = App (Abs ("x", Abs ("y", Var "x")), Var "y");;

let i = Abs ("x", Var "x");;

let w_term = Abs ("x", App (Var "x", Var "x"));;

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 paral_term = App (App (i, i), App (i, i));;

let paral_term2 = App (w_term, App (App (i, i), Var "a"));;

let print_list = iter (fun x -> print_string (x ^ "\n"));;

let fst (x, y) = x;;

let scd (x, y) = y;;

let rec string_of_lambda t =
match t with
Var a -> a
|Abs (a, Var b) when a = b -> "I"
|Abs (a, App (Var b, Var c)) when a = b && a = c -> "w"
|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"
|App (a, b) -> "(" ^ (string_of_lambda a) ^ " " ^ (string_of_lambda b) ^ ")"
|Abs (a, b) -> "(\\" ^ a ^ "." ^ (string_of_lambda b) ^ ")"
|Nil -> "NIL";;

let rec isin l a =
match l with
[] -> false
|l1::ls -> if l1 = a then true else isin ls a;;

let exclude a l = filter ((<>) a) l;;

let unique z =
let rec unique' l acc =
match l with
[] -> acc
|l1::ls -> if isin acc l1 then (unique' ls acc) else (unique' ls (l1::acc))
in unique' z [];;

let union a b = a @ filter (fun x -> not (isin a x)) b;;

let intersect c d =
fold_left (fun x y -> if isin d y then y::x else x) [] c;;

let fv z =
let rec fv' exp =
match exp with
Var a -> [a]
|App (a, b) -> (fv' a) @ (fv' b)
|Abs (a, b) -> filter (fun z -> (z <> a)) (fv' b)
|Nil -> []
in unique (fv' z);;

let cx y z =
let rec cx' a x =
if (not (isin (fv a) x)) then [] else (
match a with
Var b -> []
|App (b, c) -> (cx' b x) @ (cx' c x)
|Abs (b, c) -> (cx' c x) @ [b]
|Nil -> [] )
in unique (cx' y z);;

let rec replace a x b =
if (not (isin (fv a) x)) then a else (
match a with
Var z -> b
|App (p, q) -> App (replace p x b, replace q x b)
|Abs (y, r) -> Abs (y, replace r x b)
|Nil -> Nil );;

let rec (=@) a b =
match (a, b) with
(Var x, Var y) -> x = y
|(App (p1, q1), App (p2, q2)) -> (p1 =@ p2) && (q1 =@ q2)
|(Abs (x, p1), Abs (y, p2)) -> (replace p1 x (Var y)) =@ p2
|_ -> false;;

let rec bound_replace a x y =
match a with
Abs (z, q) -> if z = x then (Abs (y, bound_replace (replace q z (Var y)) x y)) else Abs (z, bound_replace q x y)
|App (p, q) -> App (bound_replace p x y, bound_replace q x y)
|Var z -> Var z
|Nil -> Nil;;

(* The following piece of code is not copyrighted by me *)

let union a b = a @ filter (fun x -> not (isin a x)) b;;

let rec new_name v except =
if isin except v then new_name (v ^ "'") except else v;;

let rec all_vars expr =
match expr with
Var b -> [b]
|App (p, q) -> union (all_vars p) (all_vars q)
|Abs (x, q) -> union (all_vars q) [x]
|Nil -> ["Nil"];;

(* End of non-copyrighted code *)

let rec conv_red a x b =
let cross = (intersect (cx a x) (fv b)) in
match cross with
[] -> a
|l1::ls -> conv_red (bound_replace a l1 ( new_name l1 (all_vars a) )) x b;;

let redex_reduction c =
match c with
App (Abs (x, a), b) -> if ((intersect (cx a x) (fv b)) = []) then (replace a x b) else (replace (conv_red a x b) x b)
|_ -> Nil;;

let reduct_once z =
let rec red' t =
match t with
Var a -> (false, Var a)
|Nil -> (false, Nil)
|(App (Abs (x, a), b)) as c -> let (p, q) = (red' a, red' b) in
if (not (fst p)) && (not (fst q)) then (true, redex_reduction c) else
(if (fst p) then (true, App (Abs (x, scd p), b)) else (true, App (Abs (x, a), scd q)))
|(App (a, b)) as c -> let (p, q) = (red' a, red' b) in
if (not (fst p)) && (not (fst q)) then
(false, c) else (if (fst p) then (true, App (scd p, b)) else (true, App (a, scd q)))
|(Abs (x, b)) as c -> let q = red' b in if not (fst q) then (false, c) else (true, Abs (x, scd q))
in scd (red' z);;

let parallel_reduction z =
let rec red' t =
match t with
Var b -> [Var b]
|App (Abs (x, p), q) ->
let processed = (flatten ( map (fun a ->
map (fun b -> App (Abs (x, a), b)) (red' q))
(red' p) )) in
processed @ (map (redex_reduction) processed)
|App (p, q) -> flatten ( map (fun a ->
map (fun b -> App (a, b)) (red' q))
(red' p) )
|Abs (x, r) -> map (fun a -> Abs (x, a)) (red' r)
|Nil -> [Nil]
in (red' z);;

let parallel_reduction2 z =
let rec red' t =
match t with
Var b -> Var b
|App (Abs (x, p), q) -> redex_reduction (App (Abs (x, red' p), red' q))
|App (p, q) -> App (red' p, red' q)
|Abs (x, q) -> Abs (x, red' q)
|Nil -> Nil
in (red' z);;

let normal_reduction z =
let rec red' t n =
if n > 0 then (
match t with
Var a -> (false, Var a)
|Nil -> (false, Nil)
|(App (Abs (x, a), b)) as c -> (true, redex_reduction c)
|(App (a, b)) as c -> let (p, q) = (red' a (n - 1), red' b (n - 1)) in
if (not (fst p)) && (not (fst q)) then
(false, c) else if (fst p) then (true, App (scd p, b)) else (true, App (a, scd q))
|(Abs (x, b)) as c -> let q = red' b (n - 1) in if not (fst q) then (false, c) else (true, Abs (x, scd q))
) else (false, t)
in red' z 10;;

let rec normal_form t n =
let nr = normal_reduction t in
if not (fst nr) || n = 0 then t else normal_form (scd nr) (n - 1);;

let normal_forming z =
let rec f t acc n =
let nr = normal_reduction t in
if not (fst nr) || n = 0 || isin acc (scd nr) then acc else f (scd nr) (scd nr::acc) (n - 1)
in rev (f z [] 10);;

let output redex =
print_string ("\n\nOriginal:\n" ^ (string_of_lambda redex) ^ "\n\nReducted:\n");
print_list (map (string_of_lambda) (normal_forming redex)(* ^ "\n\n"*));;

output (App (App (s, App (k, k)), k));;
output (App (w_term, w_term));;

Прикрепления: 7120826.ml (6.1 Kb)
 
iom96Дата: Среда, 07.10.2009, 21:14 | Сообщение # 2
Рядовой
Группа: Проверенные
Сообщений: 15
Репутация: 1
Статус: Offline
Во блин bash ; ну я и lol

Nobody is perfect. I'm nobody. So I'm perfect
 
  • Страница 1 из 1
  • 1
Поиск:

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