Нормализация путем оценки - Википедия - Normalisation by evaluation

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

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

Контур

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

(Типы) τ :: = α | τ1 → τ2 | τ1 × τ2

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

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

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

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

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

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

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

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

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

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

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

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

 (* отразить: 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Γ, где Γ - контекст привязок, проводится индукцией исключительно по временной структуре:

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

 (* значение: 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"))) : тм

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

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

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