Нормализация путем оценки

В языков программирования семантике нормализация путем оценки (NBE) — это метод получения нормальной формы термов λ-исчисления путем обращения к их денотационной семантике . Термин сначала интерпретируется в денотационную модель структуры λ-терма, а затем канонический (β-нормальный и η-длинный) представитель извлекается путем материализации обозначения. Такой по существу семантический подход без сокращений отличается от более традиционного синтаксического, основанного на сокращении описания нормализации как сокращения в системе переписывания терминов , где β-сокращения разрешены глубоко внутри λ-терминов.

NBE впервые был описан для просто типизированного лямбда-исчисления . С тех пор он был распространен как на более слабые системы типов , такие как нетипизированное лямбда-исчисление. с использованием теоретико-предметного подхода, а также к более богатым системам типов, таким как несколько вариантов теории типов Мартина-Лёфа .

Контур

Рассмотрим просто типизированное лямбда-исчисление , где типы τ могут быть базовыми типами (α), типами функций (→) или продуктами (×), заданными следующей грамматикой формы Бэкуса – Наура (→ сопоставление справа, как обычно):

(Типы) τ ::= a | τ ₁ → τ ₂ | т ₁ × т ₂

Они могут быть реализованы как тип данных на метаязыке; например, для Standard ML мы можем использовать:

 datatype ty = Basic of string
             | Arrow of ty * ty
             | Prod of ty * ty

Термины определяются на двух уровнях. Нижний синтаксический уровень (иногда называемый динамическим уровнем) — это представление, которое предполагается нормализовать.

(Синтаксические термины) s , t ,… ::= var x | лам ( Икс , т ) | приложение ( с , т ) | пара ( s , т ) | фст т | снд т

Здесь lam / app (соответственно пара / fst , snd ) — это формы intro / elim для → (соответственно ×), а x — переменные . Эти термины предназначены для реализации как тип данных первого порядка в метаязыке:

 datatype tm = var of string
             | lam of string * tm | app of tm * tm
             | pair of tm * tm | fst of tm | snd of tm

Денотационная семантика (закрытых) терминов метаязыка интерпретирует конструкции синтаксиса с точки зрения особенностей метаязыка; таким образом, lam интерпретируется как абстракция, app как приложение и т. д. Конструируются следующие семантические объекты:

(Семантические термины) S , T ,… ::= LAM (λ x . S x ) | ПАРА ( S , Т ) | СИН т

Обратите внимание, что в семантике нет переменных или форм исключения; они представлены просто как синтаксис. Эти семантические объекты представлены следующим типом данных:

 datatype sem = LAM of (sem -> sem)
              | PAIR of sem * sem
              | SYN of tm

Существует пара функций с индексацией типов, которые перемещаются между синтаксическим и семантическим уровнем. Первая функция, обычно обозначаемая ↑ _τ , отражает синтаксис термина в семантике, а вторая воплощает семантику как синтаксический термин (записанный как ↓ ^т ). Их определения взаимно рекурсивны следующим образом:

${\begin{aligned}\uparrow _{\alpha }t&=\mathbf {SYN} \ t\\\uparrow _{\tau _{1}\to \tau _{2}}v&=\mathbf {LAM} (\lambda S.\ \uparrow _{\tau _{2}}(\mathbf {app} \ (v,\downarrow ^{\tau _{1}}S)))\\\uparrow _{\tau _{1}\times \tau _{2}}v&=\mathbf {PAIR} (\uparrow _{\tau _{1}}(\mathbf {fst} \ v),\uparrow _{\tau _{2}}(\mathbf {snd} \ v))\\[1ex]\downarrow ^{\alpha }(\mathbf {SYN} \ t)&=t\\\downarrow ^{\tau _{1}\to \tau _{2}}(\mathbf {LAM} \ S)&=\mathbf {lam} \ (x,\downarrow ^{\tau _{2}}(S\ (\uparrow _{\tau _{1}}(\mathbf {var} \ x)))){\text{ where }}x{\text{ is fresh}}\\\downarrow ^{\tau _{1}\times \tau _{2}}(\mathbf {PAIR} \ (S,T))&=\mathbf {pair} \ (\downarrow ^{\tau _{1}}S,\downarrow ^{\tau _{2}}T)\end{aligned}}$

Эти определения легко реализуются на метаязыке:

 (* fresh_var : unit -> string *)
 val variable_ctr = ref ~1
 fun fresh_var () = 
      (variable_ctr := 1 + !variable_ctr; 
       "v" ^ Int.toString (!variable_ctr))

 (* reflect : ty -> tm -> sem *)
 fun reflect (Arrow (a, b)) t =
       LAM (fn S => reflect b (app (t, (reify a S))))
   | reflect (Prod (a, b)) t =
       PAIR (reflect a (fst t), reflect b (snd t))
   | reflect (Basic _) t =
       SYN t

 (* reify   : ty -> sem -> tm *)
 and reify (Arrow (a, b)) (LAM S) =
       let val x = fresh_var () in
         lam (x, reify b (S (reflect a (var x))))
       end
   | reify (Prod (a, b)) (PAIR (S, T)) =
       pair (reify a S, reify b T)
   | reify (Basic _) (SYN t) = t

Индукцией типа по структуре типов следует, что если семантический объект S обозначает корректно типизированный терм s τ, то овеществление объекта (т. е. ↓ ^т S) создает β-нормальную η-длинную форму s . Следовательно, остается только построить исходную семантическую интерпретацию S из синтаксического термина s . Эта операция, записанная ∥ s ∥ _Γ , где Γ — контекст привязок, выполняется путем индукции исключительно по временной структуре:

${\begin{aligned}\|\mathbf {var} \ x\|_{\Gamma }&=\Gamma (x)\\\|\mathbf {lam} \ (x,s)\|_{\Gamma }&=\mathbf {LAM} \ (\lambda S.\ \|s\|_{\Gamma ,x\mapsto S})\\\|\mathbf {app} \ (s,t)\|_{\Gamma }&=S\ (\|t\|_{\Gamma }){\text{ where }}\|s\|_{\Gamma }=\mathbf {LAM} \ S\\\|\mathbf {pair} \ (s,t)\|_{\Gamma }&=\mathbf {PAIR} \ (\|s\|_{\Gamma },\|t\|_{\Gamma })\\\|\mathbf {fst} \ s\|_{\Gamma }&=S{\text{ where }}\|s\|_{\Gamma }=\mathbf {PAIR} \ (S,T)\\\|\mathbf {snd} \ t\|_{\Gamma }&=T{\text{ where }}\|t\|_{\Gamma }=\mathbf {PAIR} \ (S,T)\end{aligned}}$

В реализации:

 datatype ctx = empty 
              | add of ctx * (string * sem)

 (* lookup : ctx -> string -> sem *)
 fun lookup (add (remdr, (y, value))) x = 
       if x = y then value else lookup remdr x

 (* meaning : ctx -> tm -> sem *)
 fun meaning G t =
       case t of
         var x => lookup G x
       | lam (x, s) => LAM (fn S => meaning (add (G, (x, S))) s)
       | app (s, t) => (case meaning G s of
                          LAM S => S (meaning G t))
       | pair (s, t) => PAIR (meaning G s, meaning G t)
       | fst s => (case meaning G s of
                     PAIR (S, T) => S)
       | snd t => (case meaning G t of
                     PAIR (S, T) => T)

Обратите внимание, что существует множество неисчерпывающих случаев; однако, если применить его к закрытому, правильно типизированному термину, ни один из этих пропущенных случаев никогда не встречается. Тогда операция НБЕ на закрытых условиях будет выглядеть следующим образом:

 (* nbe : ty -> tm -> tm *)
 fun nbe a t = reify a (meaning empty t)

В качестве примера его употребления рассмотрим синтаксический термин SKK определено ниже:

 val K = lam ("x", lam ("y", var "x"))
 val S = lam ("x", lam ("y", lam ("z", app (app (var "x", var "z"), app (var "y", var "z")))))
 val SKK = app (app (S, K), K)

Это хорошо известное кодирование функции тождества в комбинаторной логике . Нормализация его по типу идентификатора дает:

 - nbe (Arrow (Basic "a", Basic "a")) SKK;
 val it = lam ("v0",var "v0") : tm

На самом деле результат имеет η-длинную форму, как можно легко увидеть, нормализовав его к другому типу идентификатора:

 - nbe (Arrow (Arrow (Basic "a", Basic "b"), Arrow (Basic "a", Basic "b"))) SKK;
 val it = lam ("v1",lam ("v2",app (var "v1",var "v2"))) : tm

Варианты

Использование уровней де Брейна вместо имен в остаточном синтаксисе делает reify чистая функция, в которой нет необходимости fresh_var.

Тип данных остаточных термов также может быть типом данных остаточных термов в нормальной форме . Тип reify (и, следовательно, из nbe) тогда дает понять, что результат нормализован. А если тип данных нормальных форм типизирован, то тип reify (и, следовательно, из nbe) затем дает понять, что нормализация сохраняет тип.

Нормализация путем оценки также масштабируется до просто типизированного лямбда-исчисления с суммами ( +), используя операторы управления с разделителями shift и reset.

См. также

• MINLOG — помощник по проверке , использующий NBE в качестве механизма перезаписи.