diff --git a/task5/eval.ml b/task5/eval.ml new file mode 100644 index 0000000..de2269e --- /dev/null +++ b/task5/eval.ml @@ -0,0 +1,194 @@ +(* Абстрактный синтаксис для λ-исчисления: + + e ::= x + | λx.e + | e e + + В нашем конкретном синтаксисе, + + 1. λx.e заменено на fun x -> e + 2. Допускается (е). Парсер превращает это в e + 3. Допускается let x = e in e'. Парсер преврящает в (λx.e') e *) +type e = + | Variable of string + | Lambda of string * e + | Apply of e * e + +(* От абстрактного синтаксиса обратно в конкретный. *) +let rec show e = + match e with + | Variable x -> x + | Lambda (x, e) -> Printf.sprintf "(fun %s -> %s)" x (show e) + | Apply (e1, e2) -> Printf.sprintf "(%s %s)" (show e1) (show e2) + + + +(* Считывает весь стандартный вход. *) +let rec read () = + match Stdlib.read_line () with + | exception End_of_file -> "" + | s -> s ^ " " ^ (read ()) + +(* Очень плохой токенизатор. На самом деле надо использовать ocamllex или + sedlex. *) +let tokenize s = + let rec insert token strings = + match strings with + | s::s'::strings -> s::token::(insert token (s'::strings)) + | _ -> strings + in + String.split_on_char '(' s + |> insert "(" + |> List.map (String.split_on_char ')') + |> List.map (insert ")") + |> List.flatten + |> List.map (String.split_on_char ' ') + |> List.flatten + |> List.map String.trim + |> List.filter ((<>) "") + +(* Сам парсер. Первые две функции находят последовательность приложений + функций, то есть e1 e2 e3 e4... Третья разбирает каждую e1, e2, ..., + определяя, это переменная, лямбда или скобка, содержащая общее выражение. *) +let rec parse_general input = + let (e, input) = parse_non_apply input in + match input with + | ")"::_ | "in"::_ | [] -> (e, input) + | _ -> parse_apply ~e1:e input + +and parse_apply ~e1 input = + let (e2, input) = parse_non_apply input in + let e = Apply (e1, e2) in + match input with + | ")"::_ | "in"::_ | [] -> (e, input) + | _ -> parse_apply ~e1:e input + +and parse_non_apply input = + match input with + | "("::input -> + let (e, input) = parse_general input in + begin match input with + | ")"::input -> (e, input) + | _ -> failwith "unmatched '('" + end + | "fun"::x::"->"::input -> + let (e, input) = parse_general input in + (Lambda (x, e), input) + | "let"::x::"="::input -> + let (e1, input) = parse_general input in + begin match input with + | "in"::input -> + let (e2, input) = parse_general input in + (Apply (Lambda (x, e2), e1), input) + | _ -> + failwith "expected 'in'" + end + | x::input -> + (Variable x, input) + | [] -> + failwith "expected an expression" + +let parse s = + s + |> tokenize + |> parse_general + |> fst + + + +(* Интерпретатор. *) + +(* Под λx.e, в e заменяет x на y. Если е содержит λ как подвыражение, и эта + λ затеняет x, там замена не происходит. *) +let rec alpha_vary x y e = + match e with + | Variable z when z = x -> Variable y + | Variable z -> Variable z + | Lambda (z, e) when z = x -> Lambda (z, e) + | Lambda (z, e) -> Lambda (z, alpha_vary x y e) + | Apply (e1, e2) -> Apply (alpha_vary x y e1, alpha_vary x y e2) + +(* Свободные переменные выражения e. То есть те, которые не происходит от + окружающей λ. Например, в λx.x y, у свободная переменная, потому что не + происходит от окружающей её λ. Свободные переменные могут быть захвачены + внешней λ если в λ их не переименовать, то есть если наивно вычислить + (λx.λy.x у) у, результат будет λу.у у, но внешняя у не должна ссылаться на + внутреннюю y в λy. Для этого во время замены в λy.x у, внутреннюю y надо + α-переименовать используя alpha_vary в, например _у1, и результат вычисления + будет λ_у1.у _у1. *) +let rec free_variables e = + match e with + | Variable x -> [x] + | Lambda (x, e) -> List.filter ((<>) x) (free_variables e) + | Apply (e1, e2) -> (free_variables e1) @ (free_variables e2) + +(* Добавляет приблизительно уникальный суффикс к переменной. Парсер не + проверяет, что такие суффиксы не могут быть введены вручную. *) +let unique = + let last_suffix = ref 0 in + fun x -> + incr last_suffix; + Printf.sprintf "_%s%i" x !last_suffix + +(* Заменяет в e все случаи x на e'. Избегает захвата свободных переменных. + Смотрите комметарий выше у free_variables. *) +let rec substitute e e' x = + match e with + | Variable y when y = x -> e' + | Variable y -> Variable y + | Lambda (y, e'') -> + if y = x then + Lambda (y, e'') + else + let (y, e'') = + if List.mem y (free_variables e') then + let y' = unique y in + let e'' = alpha_vary y y' e'' in + (y', e'') + else + (y, e'') + in + Lambda (y, substitute e'' e' x) + | Apply (e1, e2) -> Apply (substitute e1 e' x, substitute e2 e' x) + +(* Вычисляет следующий шаг e' вычисления e. Если таковой имеется, результат + Some e'. Если вычисление невозможно, результат None. *) +let rec step e = + match e with + | Apply (Apply (Variable "print", Variable x), e) -> + print_endline x; + Some e + | Apply (Lambda (x, e1), e2) -> + begin match step e2 with + | Some e2' -> Some (Apply (Lambda (x, e1), e2')) + | None -> Some (substitute e1 e2 x) + end + | Apply (e1, e2) -> + begin match step e1 with + | Some e1' -> Some (Apply (e1', e2)) + | None -> + match step e2 with + | Some e2' -> Some (Apply (e1, e2')) + | None -> None + end + | _ -> None + +(* Многократно применяет step пока вычисление не становится невозможным. *) +let rec eval e = + match step e with + | Some e' -> eval e' + | None -> e + +(* Аналогичен eval, но выводит шаги *) +let rec trace e = + show e |> print_endline; + match step e with + | Some e' -> trace e' + | None -> e + +let _ = + read () + |> parse + |> eval + |> show + |> print_endline diff --git a/task5/numeral.lambda b/task5/numeral.lambda new file mode 100644 index 0000000..80880b9 --- /dev/null +++ b/task5/numeral.lambda @@ -0,0 +1,31 @@ +let 0 = + fun f -> fun init -> + init +in + +let +1 = + fun n -> + fun f -> fun init -> + f (n f init) +in + +let 1 = +1 0 in +let 2 = +1 1 in +let 3 = +1 2 in +let 4 = +1 3 in +let 5 = +1 4 in + +let print_n = + fun n -> + n (fun accumulator -> print foo accumulator) (fun x -> x) +in + +let + = + fun n -> fun n' -> n +1 n' +in + +let * = + fun n -> fun n' -> n (n' +1) 0 +in + +print_n (* 4 3) diff --git a/task5/test.lambda b/task5/test.lambda new file mode 100644 index 0000000..cbbb4c8 --- /dev/null +++ b/task5/test.lambda @@ -0,0 +1 @@ +(fun x -> fun y -> x) z w