![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
Функциональный апартеид
http://udpn.livejournal.com/78084.html?style=mine
Обычно говорят, что нормальный порядок редукции нужен для того, чтобы bottom в аргументе не превращался в bottom в результате всегда, когда это возможно. Само по себе это никому не нужно. Дело именно в отложенном вычислении аргументов. Чтобы определить управляющие конструкции в языке с аппл. порядком редукции, нужно это делать явно, и их можно ввести только конечное число на этапе разработки языка. С нормальным порядком мы имеем возможность определять новые конструкции в любом количестве.
Всех, кто ничего не понял - отправить в индию и бангладеш, купаться в ганге и поклонятся коровам.
Обычно говорят, что нормальный порядок редукции нужен для того, чтобы bottom в аргументе не превращался в bottom в результате всегда, когда это возможно. Само по себе это никому не нужно. Дело именно в отложенном вычислении аргументов. Чтобы определить управляющие конструкции в языке с аппл. порядком редукции, нужно это делать явно, и их можно ввести только конечное число на этапе разработки языка. С нормальным порядком мы имеем возможность определять новые конструкции в любом количестве.
Всех, кто ничего не понял - отправить в индию и бангладеш, купаться в ганге и поклонятся коровам.
no subject
Стоит заметить, что любая программа на Тьюринг-полном языке раскладывается на составляющие —
одна составляющая проверяет, что некое вычисление не ноль и повторяет его,
вторая составляющая Тьюринг-худая, и вполне бы, достаточно просто-типа-лямбды с натуральными числами.
Но вот уж завершающейся части Agda/CoQ для второй составляющеей точно достаточно.
Например, веб-сервер не должен завершаться.
Однако, его halting problem никого не волнует ;-)
А вот один шаг (ну или некоторой ограниченное число шагов) его работы (та самая Тьюринг-худая составляющая) очень даже интересно проверить на корректность, соответствие спецификации ивсётакое.