Анотація
Мова програмування
Синтаксис
Терми
I = #identifier
BOB = I | Con BOB | Dup BOB | Era BOB
| Pair (BOB, BOB) | Unit
| Let (I, BOB, BOB) | Swap BOBtype term =
| Var of string
| Con of term
| Dup of term
| Era of term
| Pair of term * term
| Swap of term
| Let of string * term * term
| UnitПравила обчислень
Обчислення в
Con (Con x) → Pair (x, x) (* ζ-ζ анігіляція: два дроти *)
Dup (Dup x) → Pair (x, x) (* δ-δ анігіляція: два дроти *)
Era (Era x) → Unit (* ε-ε анігіляція: порожня мережа *)
Con (Dup x) → Dup (Con x) (* ζ-δ комутація: перестановка *)
Con (Era x) → Pair (Era x, Era x) (* ζ-ε комутація: два ε вузли *)
Dup (Era x) → Pair (Era x, Era x) (* δ-ε комутація: два ε вузли *)
Swap (Pair (t, u)) → Pair (u, t) (* δ-ζ комутація: обмін портів *)
Let (x, t, u) → subst x t u (* Підстановка *)Синтаксис
Терми
type term =
| Var of string
| Con of term
| Dup of term
| Era of term
| Pair of term * term
| Swap of term
| Let of string * term * term
| UnitПідстановка
Підстановка в
let rec subst env var term = function
| Var v ->
if v = var then
if is_bound var env then failwith "Affine violation: variable used twice"
else term
else Var v
| Con t -> Con (subst env var term t)
| Dup t -> Dup (subst env var term t)
| Era t -> Era (subst env var term t)
| Pair (t, u) -> Pair (subst env var term t, subst env var term u)
| Swap t -> Swap (subst env var term t)
| Let (x, t1, t2) ->
let t1' = subst env var term t1 in
if x = var then Let (x, t1', t2)
else Let (x, t1', subst env var term t2)
| Unit -> UnitРедукція
Редукція виконує правила анігіляції та комутації для активних пар.
let reduce env term =
match term with
| Con (Con x) -> Pair (x, x) (* ζ-ζ анігіляція *)
| Dup (Dup x) -> Pair (x, x) (* δ-δ анігіляція *)
| Era (Era x) -> Unit (* ε-ε анігіляція *)
| Con (Dup x) -> Dup (Con x) (* ζ-δ комутація *)
| Con (Era x) -> Pair (Era x, Era x) (* ζ-ε комутація *)
| Dup (Era x) -> Pair (Era x, Era x) (* δ-ε комутація *)
| Swap (Pair (t, u)) -> Pair (u, t) (* δ-ζ комутація *)
| Let (x, t, u) -> subst env x t u (* Підстановка *)
| _ -> termПошук активних пар
Пошук усіх редукованих підтермів (активних пар) для паралельної оцінки.
let rec find_redexes env term acc =
match term with
| Con (Con x) -> (term, Pair (x, x)) :: acc
| Dup (Dup x) -> (term, Pair (x, x)) :: acc
| Era (Era x) -> (term, Unit) :: acc
| Con (Dup x) -> (term, Dup (Con x)) :: acc
| Con (Era x) -> (term, Pair (Era x, Era x)) :: acc
| Dup (Era x) -> (term, Pair (Era x, Era x)) :: acc
| Swap (Pair (t, u)) -> (term, Pair (u, t)) :: acc
| Let (x, t, u) -> (term, subst env x t u) :: find_redexes env t (find_redexes env u acc)
| Con t ->
(match t with
| Dup _ | Era _ -> acc
| Con x -> find_redexes env t ((term, reduce env term) :: acc)
| _ -> find_redexes env t acc)
| Dup t -> find_redexes env t acc
| Era t -> find_redexes env t acc
| Pair (t, u) ->
let acc' = find_redexes env t acc in
find_redexes env u acc'
| Swap t -> find_redexes env t acc
| Var _ | Unit -> accПаралельна редукція
Паралельна редукція використовує бібліотеку domainslib для одночасної обробки активних пар.
let eval_parallel pool env term =
let rec loop term =
let redexes = find_redexes env term [] in
if redexes = [] then term
else
let new_term = Task.run pool (fun () ->
List.fold_left
(fun acc (old_t, new_t) -> replace_subterm old_t new_t acc)
term redexes
) in
loop new_term
in
loop termВнутрішня мова СМК
Доведення, що представлена мова
Ці конструктори відповідають аксіомам СМК:
Лямбда функція і її аплікація в цьому численні визначаються так:
Бібліографія
[1]. Yves Lafont. Interaction Nets. 1990
[2]. Simon Gay. Interaction Nets. Diploma. 1991
[3]. Damiano Mazza. A Denotational Semantics for the Symmetric Interaction Combinators. 2006
[4]. Victor Taelin. ICVM. 2023.