Что-то пока нет в примерах ничего, что качественно отличает типизированные варианты от бестипового λ-исчисления. А ограничений вместо этого сразу накладывается целая куча. Чтобы делать анализ программ, совсем не обязательно использовать типы при их написании. Ну, а логика разве не остановилась на конструктивной линейной, из которой, собственно, и получен теоретический предел эффективности вычислений в виде оптимальной редукции?
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
no subject
Date: 2012-02-20 12:02 pm (UTC)