Юбилей у SBCL - 10 лет!

есть еще вариация вида «вектор из произвольного числа элементов и его потомок вектор из построянного числа»

> Ну разумеется, я имел ввиду только императивный выч. процесс.

's/ я / Кнут /'

state sicken

:)

> Народ, вы явно не схватываете суть. Посмотрите, как у Кнута в самом начале первого тома описывается вычислительный процесс.

это я схватил больше 20 лет назад

а сейчас меня интересует совсем другое

Кнут как раз математически корректно и описал императивный вычислительный процесс: каждый раз x - это новый x, а старого x уже нет

Любой математик за x = x + 1 башку оторвет. И труднее всего было объяснить, что старого X уже нет.

«Математически» этот алгоритм описывается вот так:

НОД(x,y) = { x, где y = 0
           { НОД(y,( x % y ))

Или ты в у нивере где-либо в матане или выводах в физике встречал итеративные обозначения? Даже значков кучи нипридумывали вроде ∑,∫,и т.д.

но интересуют только варианты с *мутабельным* прямоугольником, а иначе получится хаскель :-(

Будет нарушение LSP, если не воспринимать его чисто буквально, а по сути.

> Любой математик за x = x + 1 башку оторвет. И труднее всего было объяснить, что старого X уже нет.

Ну так и я про то же. Что смутило-то? Эта четвёрка (состояние, ввод, вывод, алгоритм)? Это четвёрка множеств, а не значений. Считайте их типами. А значения выглядят так: q0, f(q0) = q1, f(q1) = q2, ... f(qn-1) = f(qn), f(qn) = qn — завершение вычисления, неподвижная точка.

Или ты в у нивере где-либо в матане или выводах в физике встречал итеративные обозначения?

Не поверите, но да. На дискретной математике, когда я предложил свой (рекурсивный с аккумулятором) вариант решения одной задачи, меня так, видимо, никто и не понял. Официально решили с счётчиками и циклами :(

> Будет нарушение LSP, если не воспринимать его чисто буквально, а по сути.

а вот хочется и LSP, и мутабельности прямоугольника...

есть еще вариация вида «вектор из произвольного числа элементов и его потомок вектор из построянного числа»

у меня в голове крутятся только общущения вокру dependent types, и прочего специфицирования понимания наследования. То есть квадрат это такой прямоугольник который..., и не прочий.

> Любой математик за x = x + 1 башку оторвет.

Почему же? Алеф-нуль, например :)

> однако, при попытке применить это, например рассмотреть «множество всех множеств», получаем жестокий облом

Ага, а потом множество всех множеств, которые не являются элементами самих себя? :) Уже было в Симпсонах(с). Так мы получили теорию типов.

либо к конструктивным идеям «мы можем только строить из того что есть, а изначально у нас есть zero и succ»

Ба, а тут уже попахивает интуиционизмом. btw, я так и не смог в свое время понять, что за шляпа такая «свободно становящаяся последовательность». Слишком мало наркотиков было принято мной тогда. Может кто покидает вразумительными ссылками? Раз уж такая пьянка тут понеслась.

> На дискретной математике, когда я предложил свой (рекурсивный с аккумулятором) вариант решения одной задачи

Аккумулятор все испортил, точно тебе говорю. «Люсенька, родная, зараза, сдались тебе эти макароны»(с)

Пока смотрю сюда:

http://www.ats-lang.org/TUTORIAL/contents/datatypes.html

выглядит похожим. Как проснусь посмотрю подробнее:

Слишком мало наркотиков было принято мной тогда

я в процессе повышения концентрации, и интуиционизм пока что воспринимаю на уровне, гм, интуиции

> Числовой континуум трактуется не как совокупность отдельных точек, а как «среда становления», поток измельчающихся рациональных интервалов. Каждое отдельное интуиционистское вещественное число определяется как свободно становящаяся последовательность неограниченно уменьшающихся вложенных друг в друга рациональных интервалов.

хех. я всегда воспринимал вещественные числа как бесконечные десятичные дроби, и считаю, что так его и надо строить (обычные свойства вещественных чисел доказываются без труда)

ну и еще

Hilbert's program was widely held to have been seriously damaged by Gödel's Second Incompleteness Theorem, according to which the consistency of arithmetic was unprovable within arithmetic itself. But a consequence of Meyer's construction was that within his arithmetic R# it was demonstrable by simple finitary means that whatever contradictions there might happen to be, they could not adversely affect any numerical calculations.

ахренеть.

добавлю, что мои филосовские взгляды согласуются с возможностью наличия настоящих противоречий вида A && not A

почему я раньше об этом не задумывался?

ну и еще проглядывает явная польза Dialetheism-а для программирования

> я в процессе повышения концентрации, и интуиционизм пока что воспринимаю на уровне, гм, интуиции

интуиционизм не соглашается с законом исключения третьего

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

поправочка (если не ошибаюсь): s/формальной логике/закону исключения третьего/

> добавлю, что мои филосовские взгляды согласуются с возможностью наличия настоящих противоречий вида A && not A

вот только я раньше считал, что из этого должен происходить и происходит explosion, а сейчас считаю, что вопрос требует исследования

>Объектную модель лиспа сделали по образу и подобию смолтоковской, неудачный вброс

Хм, в смоллтоке были generic functions/multiple dispatch? Не знал, не знал

интуиционизм не соглашается с законом исключения третьего

капитан очевидность наносит ответный удар?

вот только я раньше считал, что из этого должен происходить и происходит explosion

есть хороший пример с теоремой Ферма в 1990, скажем, году: если взять выражение, постулируемое теоремой, за A, то утверждение (A && !A), вообще говоря, ложно - так как теорема (на тот момент) не доказана и не опровергнута

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

Ненавижу этот книжный пример. Люто-бешено

Чтобы доказать тезис, нужно либо собрать всех ворон и удостовериться, что они черные, либо собрать всех не-ворон и удостовериться, что они не черные. Так сколько же вариантов нужно для уверенности перебрать в первом случае, а сколько — во втором?

По-моему формальная логика здесь не при делах. Типичное давление на «интуиционное» мышление, но только не в том плане, который имеют ввиду интуиционисты. Давление на экспериментальность. Человек интуитивно откидывает малоосуществимые эксперименты.

> хех. я всегда воспринимал вещественные числа как бесконечные десятичные дроби, и считаю, что так его и надо строить (обычные свойства вещественных чисел доказываются без труда)

А как же пополнение метрического пространства рациональных чисел? Ну или хотя бы сечение Дедекинда?

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

fixed

Поздравляю всех адептов Lisp :)

>Программирование = математика.

руки прочь от математики.

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

это у меня руки кривые, или у cliki действительно плоховато с актуальностью базы пакетов?

Ну да, пытайся себя в этом убедить ^_^

generic functions

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

(some-action some-object)

someObject perform: #someAction

Суть близка

multiple dispatch

Integer>>+ aNumber
    ^ aNumber addInteger: self

Float>>+ aNumber
    ^ aNumber addFloat: self

Integer>>addInteger: anInteger
    "implementation here"

Float>>addFloat: aFloat
    "...and here"

Как-то примерно так

Очень нужно. Я когда-то давным-давно лисп изучал, за пару вечерков накатал подкидного дурака на двоих. Или то пролог был...

>эта новость определённо написана with an alien technology, ибо гуманоидами читается с заметным трудом

она просто переведена с лиспа на убогонький недоязычок.

>Пусть откроет для себя Symbolics Genera

если открыть дверь кунсткамеры, то можно и более queer вещи обнаружить. хотя, это да, очень странный фрукт.

> Как-то примерно так

То есть никак.

вероятно можно автоматизировать процесс метапрограммированием, я в те дебри пока не вдавался =)

> А как же пополнение метрического пространства рациональных чисел? Ну или хотя бы сечение Дедекинда?

результат то же самый. и что?

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

Т.е. конструктивно, с точки зрения опытной проверки, это два разных утверждения с двумя разными трудозатратами. Учитывая то, что наши знания базируются на опытной проверке и обладают некоторой неточностью, следовало бы *различать* эти 2 утверждения.

следовало бы *различать* эти 2 утверждения, а может и вообще не считать эквивалентными.

Можно ли в лиспе сделать х глобальной переменной и указать ей тип, чтобы:

1. переполнение при сложении и сдвиге не проверялось (нужна скорость)

В стандарте про машинные типы и взаимодействие с ними не сказано ни слова. В SBCL можно, если указать (safety 0).

2. операции боксинга-разбоксинга не осуществлялись (нужна скорость)

Если из temporary регистра значение не выходит (цикл какой-нибудь), то SBCL боксинг/разбоксинг не делает. В остальном, см. выше.

Мешает ли сделать так что-либо в каком-то из стандартов лиспа, или это недопиленные реализации?

Стандартная реализация делает всё то, что описано в стандарте. Регистров и непосредственно адресуемой памяти в стандарте не описано. Поэтому Лисп спокойно ложится практически на любой тип рантайма, который существует. Например, ABCL работает под JVM, в которой для программы доступа к железу нет.

Что касается специфичных для реализации решений, то я где-то год назад постил такой кусок кода в теме, в которой сам Саныч на лиспе пример наваял. Там для SBCL в компилятор прямо из программы добавляется низкоуровневый тип и операции над ним.

> Если из temporary регистра значение не выходит (цикл какой-нибудь), то SBCL боксинг/разбоксинг не делает. В остальном, см. выше.

переменная глобальная, будет меняться из 2 функций. что с боксингом?

> результат то же самый. и что?

Хер бы там. man p-адические числа. А для начала советую попытаться доказать, что 0.(9) = 1.0 в той постановке, если определять вещественные числа, как десятичные дроби.

даже точнее — http://www.linux.org.ru/jump-message.jsp?msgid=4254952&cid=4256112

там love5an в зависимости от оптимизации получал то 28, то 29 битов, и (далее по треду) пытался убедить меня, что 32 по стандарту не получится. я честно говоря офигел. теперь тут спрашиваю.

> Учитывая то, что наши знания базируются на опытной проверке и обладают некоторой неточностью, следовало бы *различать* эти 2 утверждения.

То есть. Тебе сказали, что в коробке лежат геометрические фигуры, причем все шары красные. Ты проковырял маленькую дырочку, увидел что-то черное. Ты не сделаешь вывод, что это не шар? Это очень странная логика должна быть.

> А для начала советую попытаться доказать, что 0.(9) = 1.0 в той постановке, если определять вещественные числа, как десятичные дроби.

а это надо ввести в определение эквивалентности, а не доказывать

можно это обосновать тем, что без этого уж точно полноты не видать

> Тебе сказали, что в коробке лежат геометрические фигуры, причем все шары красные. Ты проковырял маленькую дырочку, увидел что-то черное. Ты не сделаешь вывод, что это не шар? Это очень странная логика должна быть.

Кто мне сказал? Непогрешимый Всезнающий Бла Бла Бла?

А имеющаяся инфа идет с ошибками и упрощающими огрублениями.

(Даже вот эквивалентность двух утверждений — это тоже огрубление, правда вопрос стоит немного по-другому)

Ни-ни-ни, Девид Блейн. Если так каждую мелочь вносить в определения, очень скоро можно будет вешаться на них.

> Кто мне сказал? Непогрешимый Всезнающий Бла Бла Бла?

А имеющаяся инфа идет с ошибками и упрощающими огрублениями.

Опять же ни-ни-ни. Допустим, что сказал это тот, кто упаковывал коробку и он не врет. А то это уже нечеткая логика получается. Интуиционисты ребята чоткие, у них точно нет таких замашек. Фуззи лоджик — это явно не в ту степь.

> А то это уже нечеткая логика получается. Интуиционисты ребята чоткие, у них точно нет таких замашек.

Мне пофиг на интуиционистов. Мне интересно как думаю я.

И данный пример не является доказательством, а только наводящим соображением.

> Ни-ни-ни, Девид Блейн. Если так каждую мелочь вносить в определения, очень скоро можно будет вешаться на них

Может ты определишь, что есть мелочь, а что — не мелочь?

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

> Фуззи лоджик — это явно не в ту степь.

а тут не фуззи ложик совсем

тут вопрос «кому/чему больше верить в случае противоречия» — закону исключения третьего и непротиворечивости нашей теории, или ...

переменная глобальная, будет меняться из 2 функций. что с боксингом?

В SBCL? Разумеется, боксинг будет.