>> \alpha-, \beta- и \eta- редукции + определение нормальной формы.
>> Чистейший TRS.
> Я и обосновал. А ты не понял. Потому что ты дурак.

А, это было формальное доказательство? И я дурак после этого?

> Тождество и тождественность не различаем?
> RTFM про "Turing equivalence".

Стоп, вы использовали термин тождественности в цепочки логических рассуждений, в которых термин тождество был бы уместен (ну если бы был верен), но использовать "Turing equivalence" было бы очень глупо.

> Тебе смотреть бесполезно. Ты слеп, потому как глуп и безграмотен.

Ну примерно подобная логика присутствует во всех ваших рассуждениях, логика является алгеброй потому что я глуп, угу.

> человек, не знающий, что такое алгебра, не сможет
> сделать приличной реализации XSL

Почему? В какой реализации XSLT вы участвовали? Знаете, так случилось, что я отлично пишу на XSLT (по-крайней мере, лучше тех, с кем мне приходилось сталкиваться и у кого был подобный навык). И много работал с различными реализациями. Немного в курсе вопроса. Так что я смогу оценить, если вы мне расскажете какая реализация и за счёт какой алгебры лучше остальных, ну и чем конечно она лучше.

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

У меня около 12000 строк открытого кода, что же вы до сих пор не прошлись по мне на его основе? Только рассказываете мне какой я плохой программист, а у вас столько возможностей ткнуть пальцем!

archimag (05.03.2010 16:35:44)

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

Поправочка: изоморфны в алгебраическом смысле. Правда я уже боюсь это слово употреблять))

> Поправочка: изоморфны в алгебраическом смысле.

Хм, вы утверждаете, что лямбда-исчисление и логика первого порядка изоморфны в алгебраическом смысле?

archimag (05.03.2010 16:46:06)

> А, это было формальное доказательство?

Да. Ты спросил, где там TRS, промямлив что-то про формирование множества лямбда-термов. Я показал, что TRS состоит из \alpha-, \beta- и \eta-редукций. Всё. Куда дальше. Это и есть готовый TRS. Каждая из редукций - это одно rewrite rule. Вместе rewrite rules образуют TRS.

> И я дурак после этого?

Да, похоже, больше чем просто дурак. Ты баран. То есть, упёртый и самоуверенный дурак.

> Стоп, вы использовали термин тождественности в цепочки логических рассуждений, в которых термин тождество был бы уместен (ну если бы был верен), но использовать "Turing equivalence" было бы очень глупо.

Тебя прищемили за яйца, и ты начал бредить. У баранов это бывает. Всё типично.

Мне плевать, что там по твоему безграмотному мнению было бы логично в моих рассуждениях. Я употребил тождественность, AKA "отношение тождественности". "Тождество" тут не при делах. Не пытайся сражаться с терминами, они старше тебя и гораздо сильнее. Ты сдохнешь, а они останутся. Внуки твои подохнут, а они останутся.

> я отлично пишу

Я же говорю - баран. Самоуверенности много больше, чем ума.

> У меня около 12000 строк открытого кода, что же вы до сих пор не прошлись по мне на его основе?

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

>Как ты вообще диплом получил, если даже самыми базовыми математическими понятиями не владеешь?

Так он же физик. Физикам не дают дискретку и тем более абстрактную алгебру. Я же говорил, что Вы зря так грубо с архимагом)

> Хм, вы утверждаете, что лямбда-исчисление и логика первого порядка изоморфны в алгебраическом смысле?

Ещё немного, и наш самоуверенный баран впервые в жизни узнает о существовании тезиса Чёрча-Тьюринга.

> Так он же физик. Физикам не дают дискретку и тем более абстрактную алгебру.

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

> Я же говорил, что Вы зря так грубо с архимагом)

Он упёртый. Он заслужил. С упёртыми иначе нельзя.

> Да. Ты спросил, где там TRS

Нет, это вы сказали

И никаких обоснованных суждений об этом не привели.

> Мне плевать, что там по твоему безграмотному мнению было бы
> логично в моих рассуждениях.

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

> Я употребил тождественность, AKA "отношение тождественности"

Нет, вы оказывается употребили "эквивалентность по Тьюрингу", при этом вы также сказали, что

Теперь вы конечно сможете показать мне взаимно-однозначное преобразование между языками C и Common Lisp?

archimag (05.03.2010 17:01:35)

> Так он же физик. Физикам не дают дискретку и тем
> более абстрактную алгебру.

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

archimag (05.03.2010 17:03:17)

> Нет, это вы сказали

Нет, идиот. Я сказал:

> \alpha-, \beta- и \eta- редукции + определение нормальной формы. Чистейший TRS.

То есть, привел полную формулировку готовой к употреблению TRS.

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

Да, совсем барану яйца защемило. Баран окончательно с катушек слетел.

Уже самой простейшей логики баран не понимает. Повторяю для баранов: логика предикатов тождественна, то есть эквивалентна, то есть изоморфна лямбда-исчислению. На доступном баранам уровне, это означает, что логика предикатов выразима в терминах лямбда-исчисления, а лямбда-исчисление выразимо средствами логики предикатов. В свою очередь, лямбда-исчисление является TRS. Чтобы получить TRS из логики предикатов, достаточно приложить TRS к определению логики предикатов на лябмда-исчислении.

Если хочешь посмотреть, как конкретно логика предикатов описывается в форме TRS - читай "Term rewriting and all that", там это есть. Ну, это если ты вообще читать умеешь, конечно же, в чем я уже начинаю сомневаться.

> теперь вы конечно сможете показать мне взаимно-однозначное преобразование между языками C и Common Lisp?

Это были твои слова, идиот, а не мои.

И, да, есть взаимно однлзначное преобразование. Лисп можно компилировать в Си (см. GCL), а Си можно компилировать в виртуальную машину, исполняемую программой на Лиспе. Это для тебя, идиота, конечно же запредельно сложно, потому и не стоит тебе над этим примером ломать свою хрупкую головёшку.

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

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

Вообще, офигенно идиотское это занятие - спорить о математике с идиотом, который не желает ничего про эту самую математику читать.

Математика - это целиком и полностью искусственная конструкция. Нельзя о ней рассуждать на уровне наивной логики, что мол было бы в ней логичным, а что нет. Её можно только знать. Те, кто её создавали, дали вещам имена. Так уж принято, что этими именами и полагается пользоваться всем последующим исследователям. Нельзя говорить, что мол "я придумад интеграл, и не колышет, что это слово уже занято совсем другим понятием". Нельзя наезжать после этого на всех, кто говорит про интеграл, что они порят какую-то чушь, и что на самом деле интеграл - это - бла бла бла, которое я придумал.

Так что, идиот, иди и читай книги. И засунь свой код поглубже в жопу. Код ничего не доказывает, потому как спор терминологический. Был бы разговор о том, какой алгоритм унификации быстрее, и какие граничные условия в какой реализации не учитываются - тогда код был бы доказательством, причем единственным. А в этой дискуссии ты со своим кодом выглядишь абсолютным идиотом.

> Нет, идиот. Я сказал:
> \alpha-, \beta- и \eta- редукции + определение нормальной формы.
> Чистейший TRS.

Извините, у меня всё записано:

Сказано такое было здесь: http://www.linux.org.ru/jump-message.jsp?msgid=4607903&cid=4620332

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

Это что, доказательство того, что логика является алгеброй? Напомню если что:

> Лисп можно компилировать в Си (см. GCL), а Си можно компилировать > в виртуальную машину, исполняемую программой на Лиспе.

Вы даже не можете понять смысл термина "взаимно-однозначный"? Зачем тогда используете?

archimag (05.03.2010 17:26:18)

по моему спор идет скорее о философских категориях :)

Я изучал базовый понятия алгебры и знаком с лиспом слегка(тольк академически) . Судя по определению алгебры - к ней можно относить что угодно . В том числе и и любой язык програмирования в честаности lisp.

"Язык ЛИСП (LISP) был разработан в 1958 году американским ученым Джоном Маккарти как функциональный язык, предназначенный для обработки списков. (LISt Processing). В основу языка положен следующий математический аппарат: лямбда-исчисление Черча, алгебра списочных структур, теория рекурсивных функций."

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

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

> Это что, доказательство того, что логика является алгеброй?

Да. Потому как любая TRS является алгеброй.

> Вы даже не можете понять смысл термина "взаимно-однозначный"?

О нет, баран, это ты не можешь понять смысла взаимно-однозначного преобразования.

И ещё, баран, раз ты ввернул идиотизм про Си и CL - придумай мне тут быстренько взаимно-однозначное преобразование для машины Тьюринга и Си. Чтоб не повадно было со своим Си лезть туда, где говорят про лямбда-исчисление и машину Тьюринга.

Кстати, я правильно понимаю, что ни одну из ссылок, приведенных ранее, ты не читал, потому что "гордый" (то есть, тупой и упёртый мудак)?

> Математика - это целиком и полностью искусственная конструкция.

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

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

Нет, это вы рассуждаете на уровне бытовой логики (типо там то есть это, а это суть TRS, поэтому всё это АЛГЕБРА), я же требую истинной логики в рассуждениях, которая в математике безусловно есть.

archimag (05.03.2010 17:30:58)

> Извините, у меня всё записано:

У тебя, идиот, может и записано, а у ЛОРа записано нечто совсем другое, записано, на какое сообщение ты отвечал, когда порол чушь. Процитированная формулировка там была. Ты её, очевидно, не прочитал или проигнорировал, что говорит только о том, что ты баран.

> Ты окончательно слил, и, как и принято у баранов,
> не способен этого признать. Упёртый малолетний идиот...

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

> Си и CL - придумай мне тут быстренько взаимно-однозначное
> преобразование для машины Тьюринга и Си

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

archimag (05.03.2010 17:35:10)

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

Не лги. Ты математику не изучал никогда. Ты её "проходил", тупой баран. Потому что нельзя изучать математику, и не знать, что такое алгебра (а до середины этого флейма ты этого не знал, и потому старательно оттявкивался от требований дать определение).

> Нет, это вы рассуждаете на уровне бытовой логики (типо там то есть это, а это суть TRS, поэтому всё это АЛГЕБРА), я же требую истинной логики в рассуждениях, которая в математике безусловно есть.

Ты вообще тогда не понимаешь, что такое логика. Если A = B, а B = C, то A = C. И хоть ты башку об стену расшиби, а это всегда будет так.

Вообще, я всегда был убежден, что нет ничего хуже подонка, не способного признать, что он в чем-то был неправ. Ты как раз весьма характерный пример этого. Тебе дали ссылку на целую книгу о том, что такое TRS, что такое абстрактные алгебры, и как в этой модели рассматриваются лямбда-исчисление и логика предикатов первого порядка, но и после этого ты продолжаешь вонять. Ты подлец.

> Чем дальше вы заводили свои рассуждения в тупик

В тупике давно ты, ублюдок. От тебя вообще никаких рассуждений видно не было, только вонь про "покажите код, покажите код".

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

Ты идиот. Си машине Тьюринга не эквивалентен (у него нет бесконечной памяти). А вот лямбда-исчисление и логика предикатов машине Тьюринга эквивалентны. Так какого хрена ты, ничтожный подлец, влез со своими Си и Лиспом?

И кстати, дерьмо, почему ты пропускаешь 80% аргументов и 100% ссылок, которые тебе дают? Ты отморозок.

Вот кстати, подлец. Расскажи, почему alpha-, beta- и eta- редукции не образуют TRS. Ты так смешно от этого аргумента отмахнулся, что у меня появилось подозрение - ты просто не знаешь, что это такое! То есть, ты кричишь, что лямбда-исчисление это не TRS, но при этом ты даже не знаешь, что такое лямбда-исчисление. И кто после этого идиот?

похоже он все-таки прошел по ссылке и засомневался

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

> Потому что нельзя изучать математику, и не знать, что такое алгебра

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

> Ты вообще тогда не понимаешь, что такое логика.
> Если A = B, а B = C, то A = C

Вы используете = для таких категорий, как лямбда-исчисления и логика первого порядка, ссылаетесь при этом на эквивалентность по Тьюрингу и продолжаете утверждать, что вы что-то понимаете в математике?

> Си машине Тьюринга не эквивалентен (у него нет бесконечной памяти).

Вам не составит труда привести ссылку на раздел стандарт языка C, в котором указано ограничение по памяти?

archimag (05.03.2010 17:49:44)

> А программситу не обязательно быть математиком

С этим то тут никто и не спорит.

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

> Свои знания о математике

Успокойся уже, нет у тебя никаких знаний.

> я предпочитаю держать при себе,

В туалете томик Фихтенгольца изорванный хранишь?

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

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

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

> Вы используете = для таких категорий, как лямбда-исчисления и логика первого порядка,

Здесь "=" - транзитивное отношение эквивалентности.

> ссылаетесь при этом на эквивалентность по Тьюрингу и продолжаете утверждать, что вы что-то понимаете в математике?

Я утверждаю, что в математике ничего не понимаешь ты. И потому не имеешь права о ней рассуждать.

Изволь ответить: ты прочитал книгу? Ты можешь опровергнуть утверждение о том, что три перечисленные редукции образуют TRS? Ты можешь доказать, что логика предикатов первого порядка не эквивалентна лямбда-исчислению, не выразима в виде TRS, и, соответственно, не является алгеброй?

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

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

Ну, архимаг, ты и сказанул.

> Вы используете = для таких категорий, как лямбда-исчисления
> и логика первого порядка,
> Здесь "=" - транзитивное отношение эквивалентности.

Ой, дайте пожалуйста ссылку, где бы было объяснено, как применять "транзитивное отношение эквивалентности" по отношению к формальным система, действительно, очень интересно!

>> ссылаетесь при этом на эквивалентность по Тьюрингу
>> и продолжаете утверждать, что вы что-то понимаете в математике?
> Я утверждаю, что в математике ничего не понимаешь ты.
> И потому не имеешь права о ней рассуждать.

Вы таки понимаете, что уже много страниц назад спороли полную чушь, пробуете другую тактику?

> Ты можешь опровергнуть утверждение о том, что три перечисленные
> редукции образуют TRS?

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

archimag (05.03.2010 18:04:51)

> Но вообще мне было бы интересно посмотреть, как можно рассуждать,
> например, о каком либо парсере, и не знать ничего про конечные автоматы.

Оставим в стороне мои знания про конечные автоматы, но я действительно туп в вопросе парсинга, всем на это жаловался, но никто не хотел мне помочь, так что пришлось делать самому (и быстро) парсеры для dokuwiki и cl-closure-template. Это была счастливая случайность?

archimag (05.03.2010 18:08:52)

> Вы таки понимаете, что уже много страниц назад спороли полную чушь, пробуете другую тактику?

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

> Насколько я знаю, в логике и математике какое-либо утверждение требует формального доказательства

Каковое тебе в рыло сунули. Теперь твой ход - опровергай, или признай, что доказательство корректное, а ты идиот.

> Вы таки математик или сектант?

Сектант (или просто самоуверенный подонок?) тут только ты. Ведь это ты так старательно игнорируешь все приводимые доказательства, и продолжаешь верещать про "дайте мне доказательства".

Повторяю вопрос - ты книгу прочитал уже?

Вот пример того, что ты проигнорировал:

> Ты можешь опровергнуть утверждение о том, что три перечисленные редукции образуют TRS?

Изволь уж отвечать. А то ведёшь себя как последний подлец.

Тебе дали доказательство, записали явным образом TRS. Тебе этого мало? Тебе код написать? Ой ой, а ссылка на код ведь тоже была, на примеры из Qi II. И этого мало? А, ясно, просто это доказательство противоречит твоему убеждению, и потому ты с ним поступаешь, как и полагается барану - ты его игнорируешь.

Ты лучше расскажи, почему ты подлец?

Почему проигнорировал все ссылки про то, что такое "symbolic computation"? Решил замять тему? Не выйдет. Раз ты взялся всех поучать и раз ты считаешь себя самым умным, то уж изволь и соответствовать. Отвечай по полной программе за любую чушь, которую ты ляпнул.

> "Полной чушью" ты называешь утверждение о том

Что

http://www.linux.org.ru/jump-message.jsp?msgid=4607903&cid=4620332

> Каковое тебе в рыло сунули.
> Теперь твой ход - опровергай, или признай, что доказательство
> корректное, а ты идиот.

Лучше бы вы его не "в рыло сунули", а как-нибудь логически связали. Как-то странно опровергать то, в чём и так не было никакой логики. Собственно, вы сами и опровергли, просто тем фактом, что не смогли логически корректно связать свои рассуждения. Или вы просто плохой математик и нам стоит обратиться к настоящему специалисту, который сможет подтвердить ваши "знания"?

> Ведь это ты так старательно игнорируешь все приводимые доказательства

Напротив, я их старательно комментирую, указывая на все логические противоречия.

archimag (05.03.2010 18:18:37)

Вопрос anonymousу оппоненту archimagа: как относишься к смд методологии Щедровицкого (как занимавшемуся вопросами методологии)

> а как-нибудь логически связали.

Э нет, давай уж по порядку.

Ты сказал, что лямбда-исчисление это не TRS. Я сказал, что TRS, и записал этот самый TRS. Изволь или признать, что я прав, или опровергнуть. Не перескакивай на другую тему. Ты настолько тупой, что с любым элементом логической цепочки с тобой надо разбираться по отдельности.

> Собственно, вы сами и опровергли, просто тем фактом, что не смогли логически корректно связать свои рассуждения.

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

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

> Напротив, я их старательно комментирую, указывая на все логические противоречия.

Ну вот и начни с простого. Укажи, подлец, почему alpha-, beta- и eta- редукции не образуют TRS. То есть, опровергни моё утверждение о том, что лямбда-исчисление это TRS. Потом уже перейдем к более высокоуровневой задаче - опровержению утверждения о том, что TRS это алгебра. А уж если и этого у тебя не получится, только тогда подойдем к вопросу о том, почему логика предикатов якобы не является TRS и не является алгеброй.

> Почему проигнорировал все ссылки про то,
> что такое "symbolic computation"?

Решили вернуться к этой теме? Большая часть ваших ссылок была про математику, а не программирование. Я же приводил ссылки на литерату, которая, напротив, была посвященна символьным вычислениям в Common Lisp, одна из них, если вы забыли, прям так и называлась: "Common Lisp: мягкое введение в символьные вычисления". Вполне естественно, что символьные вычисления в алгебре существенно отличаются от символьных вычислений в языке программирования Common Lisp. С этого и начался "спор", что надо различать эти вещи. Но плохим математикам вероятно трудно заметить эту разницу.

archimag (05.03.2010 18:27:31)

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

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

> Решили вернуться к этой теме? Большая часть ваших ссылок была про математику, а не программирование.

Ссылки были про то, что понимается под термином "символьные вычисления". То есть, про то, что ты облажался.

> Я же приводил ссылки на литерату, которая, напротив, была посвященна символьным вычислениям в Common Lisp, одна из них, если вы забыли, прям так и называлась: "Common Lisp: мягкое введение в символьные вычисления".

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

И что, так сложно ответить на простой вопрос: да или нет? Книгу прочитал? Оглавление хотя бы посмотрел?

> Ты сказал, что лямбда-исчисление это не TRS.

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

> о, что ты отказываешься признавать такую логику, не значит,
> что это логически некорректно.

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

> И ты понятия не имеешь о том, что такое доказательство в математике

В них отсутствует логика?

> Ну вот и начни с простого. Укажи, подлец, почему
> alpha-, beta- и eta- редукции не образуют TRS.
> То есть, опровергни моё утверждение о том,
> что лямбда-исчисление это TRS.

Т.е. вы предлагаете мне опровегнуть утверждение, из которого никаким образом всё равно не следует, что "лямбда-исчисление это TRS"? Я же говорю, что у вас проблемы с логикой, как вам вообще удаётся заниматься математикой? Но я кажется догадываюсь: плохо.

archimag (05.03.2010 18:40:13)

Да я ж согласен. Вопрос был задан сам по себе без всякой связи с данным спором.

> Ага, ага. И там как раз про те самые символьные вычисления,
> из алгебры

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

archimag (05.03.2010 18:44:11)

> Напротив, никаких ссылок на алгебру там нет.

Ссылок нет. А символьные вычисления есть. Вот ведь забавно как, а?

> Но вы бы могли найти соответствующее определение в какой-нибудь литературе по программированию на Common Lisp и тем самым уже давно бы доказали мою неправоту.

Не смогу найти. Потому что термин "symbolic computations" в Computer Science имеет ровно одно значение, давно устоялся, и в других смыслах не употребляется. В Common Lisp у него нет своего, особого, уличного значения. Когда все (кроме ахремага) говорят про symbolic computations, то имеют в виду то же, что и википедия. Только у ахремага собственное мнение, от других отличное.

Ладно, урод. Надоел ты мне. Ненавижу подонков, не умеющих признавать свою неправоту. Книгу ты не прочитал, говорить с тобой не о чем.

Что вы делаете? Он же еще больше будет комплексовать и презирать "матан". Думаю, что настоящему математику лучше закончить первым, иначе это будет длиться вечно.

dave (05.03.2010 18:52:55)

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

Как это не следует? Ну ты и мразь...

Расскажи свою версию - каким, по твоему мнению, должно быть доказательство, что лямбда-исчисление это TRS, чтобы ты его признал (да, да, это доказательство есть в книге, которую ты отказался читать). Раз уж перечисление rewrite rules, из которых состоит лямбда-исчисление, не делает по твоему его TRS...

> если бы высказывание казалось бы сколько-нибудь корректным.

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

Блин, и ведь я это приводил как доказательство для идиотов, на пальцах. Но для такого идиота и это слишком сложно. Тогда нормальное доказательство, в виде непосредственно формулировки алгебры над термами первого порядка, идиоту тем более недоступно.

Медицина здесь бессильна. Умываю руки.

> Ссылок нет. А символьные вычисления есть. Вот ведь забавно как, а?

Я привёл код, который по моему мнению является примером символьных вычислений, и полностью соответствует тому, как это описывается в классической литературе по Common Lisp. Но какого-либо внятного комментария по поводу конкретного примера так и не получил. Но судя по вашим высказывания вы ничего не смыслите в Common Lisp

> Потому что термин "symbolic computations" в Computer Science имеет
> ровно одно значение, давно устоялся, и в других смыслах не употребляется.

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

> В Common Lisp у него нет своего, особого, уличного значения.

Оно не уличное, и не особое. s-выражения, они же symbolic expression, являются основным строительным материалом программ на Common Lisp. Эти выражения могут являться как данными, так и кодом одновременно, что позволяет формировать с помощью кода данные, а потом использовать их как код (eval). symbolic expression, а не просто списковыми структурами они называются потому, что могут содержать в себе символы. Как прикажете вообще называть вычисления над symbolic expression?

archimag (05.03.2010 19:05:37)

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

На самом деле, "настоящий математик", так похожий на всл, порет отменную чушь, чего стоит высказывание про то, first order logic - это алгебра, но тут мало народу разбирается в тонкостях математики, поэтому он выглядит увереннее и лучше какого-то уж совсем вялого и пассивного архимага.