![[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
no subject
no subject
Но управляющие конструкции - тоже только один из углов более хитрой проблемы.
no subject
Но разница между нормальным и аппликативным порядками остаётся.
no subject
Выйдет, если отказаться от тьюринг-полноты. Достаточно доказуемо останавливающихся программ.
no subject
no subject
no subject
Стоит заметить, что любая программа на Тьюринг-полном языке раскладывается на составляющие —
одна составляющая проверяет, что некое вычисление не ноль и повторяет его,
вторая составляющая Тьюринг-худая, и вполне бы, достаточно просто-типа-лямбды с натуральными числами.
Но вот уж завершающейся части Agda/CoQ для второй составляющеей точно достаточно.
Например, веб-сервер не должен завершаться.
Однако, его halting problem никого не волнует ;-)
А вот один шаг (ну или некоторой ограниченное число шагов) его работы (та самая Тьюринг-худая составляющая) очень даже интересно проверить на корректность, соответствие спецификации ивсётакое.
no subject
Цитирую Википедию (http://en.wikipedia.org/wiki/Kruskal%27s_tree_theorem): «The latter theorem ensures the existence of a rapidly growing function that Friedman called TREE, such that TREE(n) is the length of a longest sequence of n-labelled trees T1,...,Tm in which each Ti has at most i vertices, and no tree is embeddable into a later tree.
The TREE sequence begins TREE(1) = 1, TREE(2) = 3, then suddenly TREE(3) explodes to a value so enormously large that many other "large" combinatorial constants, such as Friedman's n(4), are extremely small by comparison. A lower bound for n(4), and hence an extremely weak lower bound for TREE(3), is A(A(...A(1)...)), where the number of A's is A(187196), and A() is a version of Ackermann's function: A(x) = 2↑↑...↑x with x-1 ↑s (Knuth up-arrows). Graham's number, for example, is approximately A^64(4) which is much smaller than the lower bound A^A(187196)(1).»
В общем, на практике больше не нать.
no subject
no subject
no subject
Но тут, обычно, больше интерен аспект ресурсов.
no subject
no subject
no subject
no subject