deniok: (Default)
[personal profile] deniok
О сколько нам открытий чудных дарит изучение просто типизированной чистой лямбды.

Пусть есть лямбда-терм, который может быть редуцирован к другому лямбда-терму с помощью цепочки обычных бета-редукций:

Сохраняется ли при этом тип? То есть верно ли утверждение

(Двойная стрелочка читается "бета-редуцируемо к")


Ответ: Нет, и, более того, дело даже не в нетипизируемости чего-то вроде Y-комбинатора и проблеме останова. Тип в процессе бета-редукций (aka вычислений) может измениться. Вот простейший пример:


Сама бета-редукция выглядит так

В чём тут дело? При применении канцеллятора аппликативная сущность y, определяемая выражением yz, теряется. Тип выражения становится более общим. Вот так-то :)

Date: 2008-03-28 07:35 pm (UTC)
From: [identity profile] dtim.livejournal.com
Ну не извращенцы ли эти математики? Канцелляторы, аппликативные сущности... У меня вот тут в php типы меняются в процессе вычислений без всяких комбинаторов и бета-редукций, и ничего - дельше строчки им деваться все равно некуда :).

(Что, кстати, про типизированную лямбду почитать? А то у меня в этой области явный пробел.)

Date: 2008-03-29 11:15 am (UTC)
From: [identity profile] antilamer.livejournal.com
О-хо-хо! Круто!

*вызывает дух Карри-Ховарда*

*загробным голосом*
Все значения с типом (s -> t) -> s -> s также имеют тип a -> b -> b.

Так что тип становится более общим в том смысле, что расширяется кодомен функции - однако и НЕ становится более общим в том смысле, что множество значений, имеющих такой тип, не расширяется.

Date: 2008-03-29 01:20 pm (UTC)
From: [identity profile] lomeo.livejournal.com
Забавно. Напомнило вот это.

Просто по ассоциации :-)

Profile

deniok: (Default)
deniok

February 2022

S M T W T F S
  12345
6789101112
13141516171819
20212223 242526
2728     

Style Credit

Expand Cut Tags

No cut tags
Page generated Jul. 27th, 2025 02:40 am
Powered by Dreamwidth Studios