Нормализация по оценке - Normalisation by evaluation - Wikipedia

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

NBE впервые был описан для просто типизированное лямбда-исчисление.^[1] С тех пор он был расширен до более слабых системы типов такой как нетипизированное лямбда-исчисление^[2] используя теоретическая область подход, и к более богатым системам типов, таким как несколько вариантов Теория типа Мартина-Лёфа.^[3][4]

Контур

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

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

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

 тип данных ты = Базовый из нить             | Стрелка из ты * ты             | Прод из ты * ты

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

(Термины синтаксиса) s,т,… ::= вар Икс | лам (Икс, т) | приложение (s, т) | пара (s, т) | первый т | snd т

Здесь лам/приложение (соотв. пара/первый,snd) являются вступление /Элим формы для → (соответственно ×) и Икс находятся переменные. Эти условия предназначены для реализации в качестве первый заказ на метаязыке:

 тип данных тм = вар из нить             | лам из нить * тм | приложение из тм * тм             | пара из тм * тм | первый из тм | snd из тм

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

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

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

 тип данных сем = LAM из (сем -> сем)              | ПАРА из сем * сем              | SYN из тм

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

${\displaystyle {\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}}}$

Эти определения легко реализовать на метаязыке:

 (* отразить: ty -> tm -> sem *) весело отражать (Стрелка (а, б)) т =       LAM (fn S => отражать б (приложение т (овеществлять а S)))   | отражать (Прод (а, б)) т =       ПАРА (отражать а (первый т)) (отражать б (snd т))   | отражать (Базовый _) т =       SYN т (* reify: ty -> sem -> tm *) и овеществлять (Стрелка (а, б)) (LAM S) =       позволять Икс = fresh_var () в         Лам (Икс, овеществлять б (S (отражать а (вар Икс))))       конец   | овеществлять (Прод (а, б)) (ПАРА S Т) =       Пара (овеществлять а S, овеществлять б Т)   | овеществлять (Базовый _) (SYN т) = т

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

${\displaystyle {\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}}}$

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

 (* значение: ctx -> tm -> sem *) весело смысл грамм т =       дело т из         вар Икс => искать грамм Икс       | лам (Икс, s) => LAM (fn S => смысл (Добавить грамм (Икс, S)) s)       | приложение (s, т) => (дело смысл грамм s из                          LAM S => S (смысл грамм т))       | пара (s, т) => ПАРА (смысл грамм s, смысл грамм т)       | первый s => (дело смысл грамм s из                     ПАРА (S, Т) => S)       | snd т => (дело смысл грамм т из                     ПАРА (S, Т) => Т)

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

 (* nbe: ty -> tm -> tm *) весело nbe а т = овеществлять а (смысл пустой т)

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

 вал K = лам ("Икс", лам ("у", вар "Икс")) вал S = лам ("Икс", лам ("у", лам ("z", приложение (приложение (вар "Икс", вар "z"), приложение (вар "у", вар "z"))))) вал SKK = приложение (приложение (S, K), K)

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

 - nbe (Стрелка (Базовый "а", Базовый "а")) SKK; вал Это = лам ("v0",вар "v0") : тм

Результат на самом деле имеет длину η, что легко увидеть, нормализовав его по другому типу идентичности:

 - nbe (Стрелка (Стрелка (Базовый "а", Базовый "б"), Стрелка (Базовый "а", Базовый "б"))) SKK; вал Это = лам ("v1",лам ("v2",приложение (вар "v1",вар "v2"))) : тм

Смотрите также

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

Рекомендации

1. Бергер, Ульрих; Швихтенберг, Гельмут (1991). «Обратный функционал оценки для типизированного λ-исчисления». LICS.
2. Филински, Анджей; Роде, Хеннинг Корсхольм (2004). «Обозначение нетипизированной нормализации путем оценки». FOSSACS.
3. Абель, Андреас; Эхлиг, Клаус; Дибьер, Питер (2007). "Нормализация оценкой теории типа Мартина-Лёфа с одной Вселенной" (PDF). MFPS.
4. Абель, Андреас; Коканд, Тьерри; Дибьер, Питер (2007). «Нормализация оценкой теории типа Мартина-Лёфа с типизированными суждениями о равенстве» (PDF). LICS.
5. Данви, Оливье (1996). «Типовая частичная оценка» (сжатый PostScript ). POPL: 242–257.