> Расскажи свою версию - каким, по твоему мнению, должно быть
> доказательство, что лямбда-исчисление это TRS

Логичным?

> В математике нет "кажется". Есть только логика.

Я полностью согласен. Проблема только в том, что у вас её (логики) нет.

> Если B есть подмножество A, а C эквивалентно B, то и C есть
> подмножество A. Если лямбда-исчисление есть алгебра, а логика
> предикатов эквивалентна лямбда-исчислению, то и она тоже есть алгебра.

Вот пробую понять. Формальная системой, например логика первого порядка или лямда-исчиления, являются множествами? И при этом для доказательства эквивалентности множеств (которые никакие не множества, а формальные системы) вы используете эквивалентность по Тьюрингу? Извините, я понял только то, что вы идиот.

> Блин, и ведь я это приводил как доказательство для идиотов,
> на пальцах.

И при этом сами выставили себя полным идиотом? Ну так думать надо, я не считать всех идиотами.

archimag (05.03.2010 19:13:30)

я не тот анонимус, но

> Формальная системой, например логика первого порядка или лямда-исчиления, являются множествами?

Строго говоря являются.

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

возможно :)

dave (05.03.2010 19:32:26)

> чего стоит высказывание про то, first order logic - это алгебра

Алгебра, алгебраическая конструкция - какая разница? Понятие "алгебра" очень широкое. Так что first order logic это действительно алгебра над множеством термов первого порядка.

Погуглил. Вообще психология какая-то, методология. Почему меня это могло хоть как-то коснуться? Меня математика интересует, а не треп всякий.

> Как прикажете вообще называть вычисления над symbolic expression?

В общем виде - как угодно, но только не symbolic computation. Термин занят, все свободны.

> Формальная системой, например логика первого порядка или лямда-исчиления, являются множествами?

Да.

> Алгебра, алгебраическая конструкция - какая разница? Понятие "алгебра" очень широкое.

Вообще говоря, first-order logic и не является алгебраической конструкцией (система), потому как трамвайная остановка не равна балерине, это разные вещи. Как минимум, формальная система - это упорядоченная четверка, а алгебра - пара.

> Строго говоря являются.

Хм, по роду своей деятельности/интересов мне приходилось работать с несколько другими разделами математиками (типа операторов в гильбертовом пространстве или тензорном исчислении на римановом пространстве), и возможно тут чего не понимаю, но как это понимать? Вот определение из вики (если оно не верно, поправьте его пожалуйста)

Я понимаю, что совокупность абстрактных объектов можно рассматривать как множество, но что делать с "правила оперирования"?

Но надеюсь, что для доказательство тождественности этих множеств таки нельзя использовать эквивалентность по Тьюрингу? ;)

archimag (05.03.2010 19:39:41)

> Так что first order logic это действительно алгебра над множеством термов первого порядка.

Это уже пошла отсебятина, не имеющая к математике никакого отношения. Мне кажется, ты просто не понимаешь, тех книг, которые советуешь прочитать. Спорить с такими, как ты, себе дороже.

Но она вообще сводится к ней http://en.wikipedia.org/wiki/Abstract_algebraic_logic#cite_ref-0

> Но она вообще сводится к ней http://en.wikipedia.org/wiki/Abstract_algebraic_logic#cite_ref-0

Это результат алгебраизации логики, никто и не говорил, что это невозможно, вспомни ту же булеву алгебру. Но это разные вещи, и так вольно обращаться настоящему математику с терминологией никто не позволит.

Нет, к психологии это не имеет отношения, в том то и дело что это позиционируется как научная методология

> Вот определение из вики (если оно не верно, поправьте его пожалуйста)

Вики - это не источник знаний.

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

<T, F, A, R>, где

T - алфавит теории (конечное множество базовых символов)

F - множество (перечислимое) формул (называемых также правильно построенными формулами — сокращенно, п.п.ф.), построенных из элементов с использованием некоторого набора синтаксических правил

A - множество формул, называемых аксиомами

R - конечное множество правил вывода

> Но надеюсь, что для доказательство тождественности этих множеств таки нельзя использовать эквивалентность по Тьюрингу? ;)

Это не ко мне, не я этот бред писал.

archimag, напомни, пожалуйста, приоритет (ранг) операторов имеет отношение к алгебре или нет?

> archimag, напомни, пожалуйста, приоритет (ранг) операторов имеет отношение к алгебре или нет?

Я не архимаг, но дико интересно, откуда вдруг возник такой вопрос? :)

мне непонятно, почему вопрос вызывает дикий интерес. Почему?

Эм, кстати: http://people.csail.mit.edu/jaffer/lambda.txt

>ABSTRACT: An algebraic system which includes Church's lambda calculus and currying is presented. Closures, applications, and currying are implemented using variable elimination.

>The usual connection made between the lambda calculus and algebra is to construct the integers using the lambda calculus and then construct algebraic (and other formulas) by Godelizing them.

>The system described here reverses this connection by implementing the lambda calculus in an algebraic system. It is used in the JACAL symbolic mathematics system and gives JACAL the ability to represent functions as members of the algebraic system. All of the system's operations (including simplification) can then be applied to functions as easily as to expressions.

Ну, и еще немного:

C.C. Pinter "A simple algebra of first order logic"

http://projecteuclid.org/DPubS?verb=Display&version=1.0&service=UI&handle=euc...

> C.C. Pinter "A simple algebra of first order logic"

Это примеры алгебраизации, ничего интересного, с тем же успехом можно было написать про булеву алгебру.

> напомни, пожалуйста, приоритет (ранг) операторов имеет
> отношение к алгебре или нет?

Не понял вопроса, речь идёт об операторах в языке выражения Closure Templates?

archimag (05.03.2010 21:01:46)

> мне непонятно, почему вопрос вызывает дикий интерес. Почему?

Просто он какой-то неожиданный и, лично мне не понятно с чем связанный.

В целом. А есть разница?

Я просто хочу разобраться. А что, не имеет?

> В целом. А есть разница?

Есть. Например мне не понятно, о каком приоритете операторов можно говорить в контексте Common Lisp.

archimag (05.03.2010 21:10:52)

я имел в виду приоритет операторов при редукции инфиксных выражений

> Я просто хочу разобраться. А что, не имеет?

Да наверняка, просто если намеренно искать, связи с алгеброй можно найти, где угодно. А разобраться с чем?

> я имел в виду приоритет операторов при редукции инфиксных выражений

Уточните пожалуйста как понимать "имеет отношение"? А то у нас тут небольшой клуб ценителей мат.формализма ;) и надо быть точным в формулировках.

archimag (05.03.2010 21:31:35)

ну, наверное, тебе виднее было, когда писал что твои символьные вычисления не имеют никакого отношения к алгебре. Вот ты и скажи, что ты понимаешь под "иметь отношение" :)

> ну, наверное, тебе виднее было, когда писал что твои символьные
> вычисления не имеют никакого отношения к алгебре. Вот ты и скажи,
> что ты понимаешь под "иметь отношение" :)

Хм, я имел ввиду, например, преобразование символьного представления шаблонов в код на Common Lisp или JavaScript, преобразование тестов для Common Lisp в тесты для JavaScript. Или поиск подходящего маршрута с помощью унификации в cl-routes. При чём тут приоритет операторов?

archimag (05.03.2010 21:50:15)

хм. вот в таком виде, чисто конкретно: то, что + и - между собой ассоциативны, а + и * -- нет, имеет отношение к алгебре?

> хм. вот в таком виде, чисто конкретно: то, что + и - между собой
> ассоциативны, а + и * -- нет, имеет отношение к алгебре?

Полагаю что да, но какое это имеет отношения к предмету?

archimag (05.03.2010 22:15:34)

Ты предложил показать тебе в твоем коде что-то имеющее отношение к алгебре.

Возьмем функцию reduce-infix из expressions.lisp, а также посмотрим на *infix-ops*. Функция reduce-infix преобразует выражения основываясь на приоритете операторов.

Как ты только что заметил, это имеет отношение к алгебре.

=> Твой код имеет отношение к алгебре.

> Возьмем функцию reduce-infix из expressions.lisp, а также
> посмотрим на *infix-ops*. Функция reduce-infix преобразует выражения
> основываясь на приоритете операторов
> => Твой код имеет отношение к алгебре.

Вообще-то, этот код имеет отношение к реализуемой спецификации, а алгебра это абстракция, так в чём суть утверждения?

archimag (05.03.2010 22:27:18)

>bla-bla-bla, мои символьные вычисления не имеют отношения к алгебре

>bla-bla-bla, мой код символьных вычислений имеет отношение к алгебре, а еще относится к реализуемой спецификации, bla-bla-bla

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

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

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

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

Или к арифметике? cl-closure-template допускает только арифметические вычисления, никаких символьных операций.

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

Вообще, с тем же успехом я могу утверждать, что это имеет отношение к квантовой механике, ибо выполнение любой программы на компьютере полностью описывается волновой функцией. И могу развить до ВОЛНОВОЙ ФУНКЦИИ (которая ещё круче АЛГЕБРЫ), описывающей всю вселенную.

archimag (05.03.2010 22:45:10)

Веселый и доброжелательный флейм начался с фразы архимага:

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

Собственно, именно потому что найти *хоть какое-то* отношение к алгебре довольно легко, все и завертелось :)

> Лисп рулил (и до сих пор рулит) в другой связанной с AI областью - computer algebra systems, то бишь, символьная математика.

Где лучше всего? Где Maxima? Упоминается символьная математика, а не символьные вычисления.

Или лисп не рулит в CAS? Вроде, очень даже. Но нет, хотелось ведь cl-closure-template похвалиться, который, дескать, к алгебре отношения не имеет.

> Собственно, именно потому что найти *хоть какое-то* отношение > к алгебре довольно легко, все и завертелось :)

Завертелось не с этого. Было сказано

Эта фраза и послужила основным леймотивом флейма

> Но нет, хотелось ведь cl-closure-template похвалиться

Нет, я говорил выше мою причину: люди ничего не смыслящие в Common Lisp постоянно несут про него всякую чушь.

archimag (05.03.2010 23:03:19)

symbolic computation вполне может существовать отдельно от лиспа, хоть common, хоть exclusive.

но, похоже, ты для себя определил symbolic computations исключительно как "операции с типом данных symbol в CL"

Таки и не продвинулись в понимании практических выводов из алгебраической точки зрения. А так все хорошо начиналось. Жесть;)

В тот момент речь ещё шла о Common Lisp, а не об АЛГЕБРЕ.

archimag (05.03.2010 23:07:41)

> похоже, ты для себя определил symbolic computations исключительно
> как "операции с типом данных symbol в CL"

Если разговор идёт в контексте Common Lisp, то как прикажете ещё понимать?

archimag (05.03.2010 23:08:54)

> Или лисп не рулит в CAS? Вроде, очень даже.

По инерции, maple, mathcad, gap4 уже пишут на сях и жабах, а аксиому и фрикас собираются переписывать на хаскелле, если я не ошибаюсь. Кроме того, например, в openaxiome, которую я смотрел год назад, ядро было написано не на Common Lisp, а на каком-то очень узком и очень древнем LISP'е, т.е. это полностью legacy код, доставшийся в наследство с 80ых годов. А практически все функции и вся обвязка написаны на своем языке aldor или spad, чисто лисп кода очень немного.

> Но нет, хотелось ведь cl-closure-template похвалиться, который, дескать, к алгебре отношения не имеет.

А он действительно, имеет слабое отношение к алгебре, если я правильно понял, что это за штука такая.

Речь шла о том, рулит ли лисп в *символьной математике* и CAS. И анонимус не конкретизировал, CL там, Scheme или еще какой лисп.

>Если разговор идёт в контексте Common Lisp, то как прикажете ещё понимать?

хм, к примеру: как операции над множеством символов?

> но, похоже, ты для себя определил symbolic computations исключительно как "операции с типом данных symbol в CL"

Не вижу тут проблемы, это такой же неоднозначный термин, как и functional programming, например :). Тут достаточно просто договориться кто и что имеет в виду, неужели столько флейма из-за этого?

> Таки и не продвинулись в понимании практических выводов из алгебраической точки зрения. А так все хорошо начиналось. Жесть;)

Если вам интересны приложения сурового матаны и дискретки, то, например, можете почитать про Coq, agda, acl2, они про автоматические доказательства корректности программы, можете почитать про автоматический неявный вывод типов Хиндли-Милнера, про System F, про оптимизации при использовании ленивых вычислений, и тд и тп.