Функциональный апартеид

[metaclass]

http://udpn.livejournal.com/78084.html?style=mine
Обычно говорят, что нормальный порядок редукции нужен для того, чтобы bottom в аргументе не превращался в bottom в результате всегда, когда это возможно. Само по себе это никому не нужно. Дело именно в отложенном вычислении аргументов. Чтобы определить управляющие конструкции в языке с аппл. порядком редукции, нужно это делать явно, и их можно ввести только конечное число на этапе разработки языка. С нормальным порядком мы имеем возможность определять новые конструкции в любом количестве.

Всех, кто ничего не понял - отправить в индию и бангладеш, купаться в ганге и поклонятся коровам.

Comments

[sleepy-drago.livejournal.com]

+1

[akuklev.livejournal.com]

Реально достаточно. На агде и родственных языках заведомо определяются все функции для которых можно дать оценку сверху скорости выполнения, которая выразима в терминах обобщённых функций Гудштейна (http://en.wikipedia.org/wiki/Goodstein's_theorem). То есть любые алгоритмы даже со временем работы O(2^2^...^n) туда влезают. Влезают любые фукнции Акермана, стрелки Конвея и чёртзнаетчто. Я слышал лишь про одну тотальную функцию, которую так построить невозможно — функцию TREE Фридмана.

Цитирую Википедию (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).»

В общем, на практике больше не нать.

[antontsau.livejournal.com]

доктор, вы маньяк.

[thesz.livejournal.com]

Уровень do-нотации делается с помощью... do-нотации!

Точнее, с помощью её разворачивания в комбинаторы. Чуть было не сделал, кстати, для одного варианта описания железа, где требовалось следить за количеством промежуточных проводов.

А далее можно и синтаксис с помощью квазиквотеров прикрутить, если надо усложнение работы.

Хотя я согласен, что DSL в Хаскеле слабоваты.

[udpn.livejournal.com]

Здесь я, похоже, слился, потому что Сoq видел полтора раза в жизни. Это там в Notation вставка ML'я? Как это сказывается на корректности программ? Сам Coq-то ленивый?

[udpn.livejournal.com]

А можно пример, на котором эта разница будет видна? Или лучше спросить самого codedot?

[udpn.livejournal.com]

"Абстрактная семантика"?

[jakobz.livejournal.com]

Всех, кто ничего не понял - отправить в индию и бангладеш, купаться в ганге и поклонятся коровам.

[gds.livejournal.com]

в Notation -- вставка того же Coq'а. Символы cond/th/el -- выражения, они не обязаны быть значениями и не обязаны вычисляться, они просто подставляются, почти синтаксически. На корректности сказывается как любой другой Coq код.
В do-нотации, если по памяти, у меня было как-то так: Notation "a <- b ;; c" := "bind (fun a => c) b", то есть, "a" рассматривается как идентификатор, и везде, где используется эта нотация, данное ограничение учитывается.
Сам Coq -- скорее строгий. Впрочем, 1. касаемо доказательств и редукций: есть тактики для ленивой работы с пруф-термами, для ленивой редукции, 2. в некоторых местах он при экстракции в окамл использует лентяйку, сходу помню экстракцию всяких коиндуктивных типов данных и работу с ними. Вот тут мне надо было бы толком разобраться, почему там лентяйка, а то понятно только интуитивно, но никак не чётко.

[m e (from livejournal.com)]

это я к тому, что получается уже не апартеид, а кастовая система:

1. кто не понял высказывание

2. кто понял высказывание, но не понял, что оно неверное

3. кто понял высказывание, и понял, что оно неверное

как вариант, можно ни апартеид, ни кастовую систему не вводить, и оставить всех на своих местах :-)

[nivanych.livejournal.com]

Я лично не против ;-)

[nivanych.livejournal.com]

А тестировать кто за них будет?

[nivanych.livejournal.com]

Ви так говорите, как будто, в этом есть что-то плохое!

[tzirechnoy.livejournal.com]

Да, попробую расшыфровать своё возмущение: у меня есть сильное подозрение, что слова "язык с аппл. порядком редукции" не имеют не то что чёткого -- дажэ вменяемого определения, и применение термина "порядок редукцыи" по отношэнию к языкам можэт иметь смысл только после какого-то частного (одного из многих) отображэния языка (включая семантику) на лямбда-исчисление.

[metaclass.livejournal.com]

Хорошо доказанные программы в тестировании не нуждаются.
Поэтому тестерш переквалифицируют в службу поддержки мозгов тех, кто эти доказанные программы пишет. Поддержка осуществляется таким образом, что бывшие тестерши очень быстро уходят в декрет.

[udpn.livejournal.com]

Да я пытаюсь понять, как это называется на самом деле, и всего-то.

[nivanych.livejournal.com]

Это неправда.
Бывают ещё и логические ошибки, а их сложно убрать доказательствами.
Кроме того, можно забыть написать нужные типы для доказательств.
То есть, хотя и всё сформулированное доказано, но сформулировано не всё.

Однако, в целом, мысль мне нравится! ;-)

[nponeccop.livejournal.com]

Лучше спросите самого лэмпинга

http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.90.2386

Levy[4, 5] has shown that there are lambda expressions for which any order of reduction duplicates work. One
example is ...

[nivanych.livejournal.com]

Да вроде бы, описания потребления ресурсов (CPU-memory-traffic) программой в разные моменты времени всегда обзывалось ресурсной семантикой...

[nivanych.livejournal.com]

"Evaluation" происходит в лямбде или в графе.
Поэтому, если язык представляет собой отображение на лямбду, то про редкуции и судят по лямбде или по graph-rewriting-системе.
Если подходить к вопросу с особенной выдумкой, то можно придумать исключение. Но вполне можно говорить, что трансляция в итоговую исполнительную машинку всегда происходит этапами.
Подобный вопрос вообще может иметь место довольно редко. Впрочем, даже и понятно, в каких случаях.
Что не так?

[tzirechnoy.livejournal.com]

>Поэтому, если язык представляет собой отображение на лямбду,

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

[nivanych.livejournal.com]

Действительно, он берёт случайные числа, собранные системой.
И они влияют на ход компиляции. А откуда вы знали?