Из Википедии, бесплатной энциклопедии
Перейти к навигации Перейти к поиску

В информатике говорят , что лямбда-исчисления имеют явные подстановки, если они уделяют особое внимание формализации процесса подстановки . Это контрастирует со стандартным лямбда-исчислением, где подстановки выполняются бета-редукцией неявным образом, который не выражается в исчислении. Концепция явных подстановок стала печально известной (несмотря на большое количество опубликованных исчислений явных подстановок в литературе с совершенно разными характеристиками), потому что это понятие часто встречается (неявно и явно) в формальных описаниях и реализации всех математических форм подстановки.с участием переменных, таких как абстрактные машины , логика предикатов и символьные вычисления .

Обзор [ править ]

Простым примером лямбда-исчисления с явной заменой является «λx», который добавляет одну новую форму термина в лямбда-исчисление , а именно форму M⟨x: = N⟩, которая читается как «M, где x будет заменен на N». . (Значение нового термина такое же, как и распространенная идиома let x: = N в M из многих языков программирования.) Λx можно записать с помощью следующих правил переписывания :

  1. (λx.M) N → M⟨x: = N⟩
  2. x⟨x: = N⟩ → N
  3. x⟨y: = N⟩ → x (x ≠ y)
  4. (M 1 M 2 ) ⟨x: = N⟩ → (M 1 ⟨x: = N⟩) (M 2 ⟨x: = N⟩)
  5. (λx.M) ⟨y: = N⟩ → λx. (M⟨y: = N⟩) (x ≠ y и x не свободен в N)

Делая подстановку явной, эта формулировка по-прежнему сохраняет сложность «соглашения о переменных» лямбда-исчисления , требуя произвольного переименования переменных во время сокращения, чтобы гарантировать, что условие «(x ≠ y and x not free in N)» в последнем правиле выполняется всегда доволен перед применением правила. Поэтому многие исчисления явной подстановки вообще избегают имен переменных, используя так называемую " безымянную" нотацию индекса Де Брёйна .

История [ править ]

Явные замены были описаны в предисловии к книге Карри по комбинаторной логике [1] и выросли из «уловки реализации», используемой, например, AUTOMATH , и стали респектабельной синтаксической теорией в лямбда-исчислении и теории переписывания . Хотя это на самом деле произошло с де Брейна , [2] идея конкретного исчисления , где замены являются частью объектного языка, а не неофициальной метатеории, традиционно приписывают к Абади , Карделли , Кюрьен и Lévy. Их основополагающая статья [3] по исчислению λσ объясняет, что реализации лямбда-исчислениянужно быть очень осторожным, имея дело с заменами. Без сложных механизмов для разделения структуры замены могут вызвать взрывной рост размера, и поэтому на практике замены задерживаются и явно записываются. Это делает соответствие между теорией и реализацией весьма нетривиальным, а правильность реализаций может быть трудно установить. Одно из решений - сделать замены частью исчисления, то есть иметь исчисление явных замен.

Однако после того, как подстановка сделана явной, основные свойства подстановки меняются с семантических на синтаксические. Одним из наиболее важных примеров является «лемма о подстановке», которая с обозначением λx принимает вид

  • (M⟨x: = N⟩) ⟨y: = P⟩ = (M⟨y: = P⟩) ⟨x: = (N⟨y: = P⟩)⟩ (где x ≠ y и x не свободен в P )

Удивительный контрпример, сделанный Меллиесом [4], показывает, что способ, которым это правило закодировано в исходном исчислении явных подстановок, не сильно нормализует . После этого было описано множество исчислений, пытающихся предложить лучший компромисс между синтаксическими свойствами явных исчислений подстановки. [5] [6] [7]

См. Также [ править ]

Ссылки [ править ]

  1. ^ Карри, Хаскелл; Фейс, Роберт (1958). Комбинаторная логика Том I . Амстердам: Издательская компания Северной Голландии.
  2. ^ NG de Bruijn: безымянное лямбда-исчисление с возможностями для внутреннего определения выражений и сегментов. Технологический университет Эйндховена, Нидерланды, математический факультет, (1978), (TH-Report), номер 78-WSK-03.
  3. ^ М. Абади, Л. Карделли, PL. Curien и JJ. Леви, Явные замены, Журнал функционального программирования 1, 4 (октябрь 1991 г.), 375–416.
  4. ^ PA. Меллиес: Типизированные лямбда-исчисления с явными заменами не могут завершаться. TLCA 1995: 328–334
  5. ^ П. Лесканн, От λσ к λυ: путешествие по исчислениям явных подстановок, POPL 1994, стр. 60–69.
  6. ↑ KH Rose, Explicit Substitution - Tutorial & Survey, BRICS LS-96-3, сентябрь 1996 г. ( ps.gz ).
  7. ^ Делия Кеснер: теория явных замен с безопасным и полным составом. Логические методы в компьютерных науках 5 (3) (2009)