Здравствуйте, _hum_, Вы писали:
__>Здравствуйте, deniok, Вы писали:
D>>Та аналогия, которую вы пытаетесь провести вслед за Митчеллом, что вычисления под dynamic scoping похожи на порченную отсутствием альфа-конверсии бета-редукцию, она да, имеет место. Только я ничего фундаментального в ней не вижу, да и Митчелл тоже не особо это наблюдение использует в дальнейшем.
__>Фундаментальность (по крайней мере для меня) в том, что из-за наличия требования альфа-конверсии лямбда-исчисление принципиально не допускает моделирования вычислений с динамическим связыванием. Получается, что лямбда-исчисление "затачивалось" под моделирование языков только со статическим связыванием. А если так, то на чем же тогда, интересно, строится теория языков с динамическим связыванием?
Ох, ну это же максимализм. То, что нет простого прямого изоморфизма, не означает, что в лямбда-исчислении нельзя построить соответствующую модель.
Re[20]: Базовые концепты computer science на примере λ-исчисления
Здравствуйте, deniok, Вы писали:
D>Здравствуйте, _hum_, Вы писали:
__>>Здравствуйте, deniok, Вы писали:
D>>>Та аналогия, которую вы пытаетесь провести вслед за Митчеллом, что вычисления под dynamic scoping похожи на порченную отсутствием альфа-конверсии бета-редукцию, она да, имеет место. Только я ничего фундаментального в ней не вижу, да и Митчелл тоже не особо это наблюдение использует в дальнейшем.
__>>Фундаментальность (по крайней мере для меня) в том, что из-за наличия требования альфа-конверсии лямбда-исчисление принципиально не допускает моделирования вычислений с динамическим связыванием. Получается, что лямбда-исчисление "затачивалось" под моделирование языков только со статическим связыванием. А если так, то на чем же тогда, интересно, строится теория языков с динамическим связыванием?
D>Ох, ну это же максимализм. То, что нет простого прямого изоморфизма, не означает, что в лямбда-исчислении нельзя построить соответствующую модель.
Построить то, конечно, можно (в силу "равномощности" "лямбд" любой другой тьюринг-полной выч. системе). Другое дело, что от модели ожидается, чтобы она была проще изучаемого объекта, иначе, какой в ней смысл.
И кстати, почему бы не ввести какое-нибудь лямбда'-исчисление, в котором обязательное требование альфа-конверсии заменить чем-нибудь более гибким, чтобы позволить в этом языке естественно описывать и статическое, и динамическое связывание? Что-нибудь про такой вариант известно?
И еще, на чем (на какой простой выч. модели) все-таки тогда строится теория языков с динамическим связыванием?