Re[19]: Базовые концепты computer science на примере λ-исчисления
От: deniok Россия  
Дата: 13.01.13 22:16
Оценка:
Здравствуйте, _hum_, Вы писали:

__>Здравствуйте, deniok, Вы писали:


D>>Та аналогия, которую вы пытаетесь провести вслед за Митчеллом, что вычисления под dynamic scoping похожи на порченную отсутствием альфа-конверсии бета-редукцию, она да, имеет место. Только я ничего фундаментального в ней не вижу, да и Митчелл тоже не особо это наблюдение использует в дальнейшем.


__>Фундаментальность (по крайней мере для меня) в том, что из-за наличия требования альфа-конверсии лямбда-исчисление принципиально не допускает моделирования вычислений с динамическим связыванием. Получается, что лямбда-исчисление "затачивалось" под моделирование языков только со статическим связыванием. А если так, то на чем же тогда, интересно, строится теория языков с динамическим связыванием?


Ох, ну это же максимализм. То, что нет простого прямого изоморфизма, не означает, что в лямбда-исчислении нельзя построить соответствующую модель.
Re[20]: Базовые концепты computer science на примере λ-исчисления
От: _hum_ Беларусь  
Дата: 14.01.13 09:48
Оценка:
Здравствуйте, deniok, Вы писали:

D>Здравствуйте, _hum_, Вы писали:


__>>Здравствуйте, deniok, Вы писали:


D>>>Та аналогия, которую вы пытаетесь провести вслед за Митчеллом, что вычисления под dynamic scoping похожи на порченную отсутствием альфа-конверсии бета-редукцию, она да, имеет место. Только я ничего фундаментального в ней не вижу, да и Митчелл тоже не особо это наблюдение использует в дальнейшем.


__>>Фундаментальность (по крайней мере для меня) в том, что из-за наличия требования альфа-конверсии лямбда-исчисление принципиально не допускает моделирования вычислений с динамическим связыванием. Получается, что лямбда-исчисление "затачивалось" под моделирование языков только со статическим связыванием. А если так, то на чем же тогда, интересно, строится теория языков с динамическим связыванием?


D>Ох, ну это же максимализм. То, что нет простого прямого изоморфизма, не означает, что в лямбда-исчислении нельзя построить соответствующую модель.


Построить то, конечно, можно (в силу "равномощности" "лямбд" любой другой тьюринг-полной выч. системе). Другое дело, что от модели ожидается, чтобы она была проще изучаемого объекта, иначе, какой в ней смысл.

И кстати, почему бы не ввести какое-нибудь лямбда'-исчисление, в котором обязательное требование альфа-конверсии заменить чем-нибудь более гибким, чтобы позволить в этом языке естественно описывать и статическое, и динамическое связывание? Что-нибудь про такой вариант известно?

И еще, на чем (на какой простой выч. модели) все-таки тогда строится теория языков с динамическим связыванием?
Подождите ...
Wait...
Пока на собственное сообщение не было ответов, его можно удалить.