LINUX.ORG.RU
ФорумTalks

Перельман.

 , matrixxx


0

2

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

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

Прошли годы и «моя ко мне вернулась» ((С)«Буммер»). Я прочитал простое объяснение ‎гипотезы Пуанкаре.

Собственно сабж.



Последнее исправление: anonimous (всего исправлений: 1)
Ответ на: комментарий от Absurd

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

anonimous
() автор топика
Ответ на: комментарий от emulek

полная практическая бесполезность

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

anonimous
() автор топика
Ответ на: комментарий от emulek

Ну народ так делал. Успешно вроде-бы. Проблема у этого проекта в общем-то только одна — полная практическая бесполезность.

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

http://visionary.stanford.edu/classes/csxyz/problems/solutions/004/released/0...

Absurd ★★★
()
Ответ на: комментарий от anonimous

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

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

Тут весь вопрос: куда идёт выход. Если в машину, то всё нормально. Если человеку — увы. Человеку такие алгоритмы не нужны.

И да, доказательство теоремы по сути — трансляция исходного текста на «языке теорем» в «язык аксиом». Что-то вроде компиляции программы на питоне в программу в машинных кодах (или в байткоде, не важно).

emulek
()
Ответ на: комментарий от Absurd

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

wtf?

emulek
()
Ответ на: комментарий от emulek

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

wtf?

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

Absurd ★★★
()
Ответ на: комментарий от Absurd

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

anonimous
() автор топика
Ответ на: комментарий от anonimous

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

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

Absurd ★★★
()
Ответ на: комментарий от anonimous

реляционный фитч

Это че такое, если попроще?

Кванторы и отношения.

Absurd ★★★
()
Ответ на: комментарий от Absurd

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

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

Такое говно я тебе могу на php набросать, за сотку $, если тебе так уж НАДО. СБИШ конечно.

emulek
()
Ответ на: комментарий от emulek

трансляция исходного текста на «языке теорем» в «язык аксиом»

А вот такая трансляция подрадает под твое определение? если нет то почему?

if (write == a) then print b
if (write == b) then print c
anonimous
() автор топика
Ответ на: комментарий от emulek

Такое говно я тебе могу на php набросать, за сотку $

Стенфорд это говно за 70$ распространяет. Хотелось бы нахаляву. Придется самому писать.

Absurd ★★★
()
Ответ на: комментарий от anonimous

трансляция исходного текста на «языке теорем» в «язык аксиом»

А вот такая трансляция подрадает под твое определение? если нет то почему?

if (write == a) then print b
if (write == b) then print c

попадает. Это условие, что тут особенного? while() тоже попадает, как и function. В принципе, достаточно только function, но это извращение (LISP, да). Извращение потому, что вход/выход обычно заточены под «процедурный подход», доказательство теоремы Пифагора в ФП — это ППЦ для неподготовленной учительницы будет...

emulek
()
Ответ на: комментарий от Absurd

Стенфорд это говно за 70$ распространяет.

А я за $5. Ну а ещё $95 я беру за СБИШ специально для тебя.

Придется самому писать.

вот и молодец.

emulek
()
Ответ на: комментарий от emulek

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

anonimous
() автор топика
Ответ на: комментарий от anonimous

Но ведь ты же не знаешь, что значит А в исходном языке и B в языке назначения

ну и что? Узнаю. Какая разница-то?

Тебе не кажется, что этого маловато для того, чтобы нзывать это доказательством. Не логичней ли будет говорить о том, что мы должны изобрести язык А, язык B, и мостик-транслятор между ними. Т.е. эту тройку и называть доказательством.

для геометрии «язык А» и «язык Б» уже изобретены. Второй — это и есть аксиомы, а первый — теоремы. «Мостик» — транслятор. Правила построения «мостика» вбивают во время школьного курса, на самом деле они довольно простые. Другое дело, что сами учителя этого не понимают, потому и получается «демагогия и натяжки», как ты говоришь. Очень сложно логично объяснить то, чего сам не понимаешь...

Ну вот нагугли «доказательство равенства треугольников по трём сторонам» из школьного курса, и обрати внимание, что это доказательство не имеет никакого отношения к аксиомам Евклида. На самом деле, доказательство построено не на аксиомах, а на их следствиях. Их в школе тоже проходят, но явно не формализуют. В итоге школьники не видят истинной картины. Может это и фича, школьник сам должен догадаться, я без понятия. Факт в том, что нынешнее поколение учителей (как и позапрошлое) само не видит связи, она(связь) утеряна. Потому и воспринимается обычно как бессмысленное нагромождение догм. Которое можно только вызубрить.

emulek
()
Ответ на: комментарий от emulek

В принципе, достаточно только function, но это извращение (LISP, да)

(define if_ (lambda(a b c) (a b c)))
(define true (lambda(x y) x))
(define false (lambda(x y) y))

(write (if_ true 1 2)) --> 1
(write (if_ false 1 2)) --> 2

Если да, то почему LISP? По-мойму, на любом ЯП с ФВП такое прокатит вполне.

И че то, я не понял вот это:

вход/выход обычно заточены под «процедурный подход»

Приведи простой пример, где процедурный подход тут рулит.

anonimous
() автор топика
Ответ на: комментарий от emulek

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

anonimous
() автор топика
Ответ на: комментарий от anonimous

Если да, то почему LISP? По-мойму, на любом ЯП с ФВП такое прокатит вполне.

Тьюринг доказал, что на чём угодно прокатит, хоть на brainfuck'е.

вход/выход обычно заточены под «процедурный подход»

Приведи простой пример, где процедурный подход тут рулит.

x86.

Ну и геометрия тоже — набор процедур и условий. Линейный. Ещё и подпрограммы есть, называются «леммы».

emulek
()
Ответ на: комментарий от emulek

x86

Я в этом не силен, можешь привести псевдокод какой нибудь?

Линейный

Мы опять возвратились к тому спору итерация vs рекурсия. Я там писал уже, если ты помнишь, что линейность точно также может быть представлена функционально. Разницы принципиальной тут нет. (Память не рассматриваем - это уже детали)

anonimous
() автор топика
Ответ на: комментарий от anonimous

Да, я согласен, но я немного о другом. Сам транслятор и процесс трансляции, на мой взгляд, не корректно называть доказательством, безотносительно самих языков. Он есть лишь инструмент

да.

доказательство — выхлоп транслятора.

1. вход: если A1B1==A2B2 && B1C1==B2C2 && C1A1==C2A2, то A1B1C1==A2B2C2

2. выход: тоже самое, но записанное в терминах аксиом Евклида.

Вот п2 это и есть «доказательство».

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

могу. Потому и говорю, что аксиомы Евклида нужны IRL, и прямо связаны с RL. Эти аксиомы — одна из моделей RL. Конечно не всего сразу, а только некоторой части, да ещё и в маленьких масштабах (из-за кривизны пространства/времени).

emulek
()
Ответ на: комментарий от emulek

доказательство — выхлоп транслятора.

Да ни хрена. Выхлоп - он и есть выхлоп. Когда ты доказываешь теорему в мат-ке, у тебя тоже есть выхлоп: «ЧТД». Это не док-во, а его результат.

anonimous
() автор топика
Ответ на: комментарий от anonimous

Я в этом не силен, можешь привести псевдокод какой нибудь?

да там всё просто: набор регистров AX,BX,CX,DX. Ну и набор операций типа ADD AX,BX (AX:=AX+BX). Есть ещё переходы, т.е. запись в регистр IP. Например JAMP 0x12345 === MOV IP, 0x12345

всё это легко гуглится.

Мы опять возвратились к тому спору итерация vs рекурсия. Я там писал уже, если ты помнишь, что линейность точно также может быть представлена функционально. Разницы принципиальной тут нет.

(Память не рассматриваем - это уже детали)

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

emulek
()
Ответ на: комментарий от anonimous

Да ни хрена.

учись читать...

1. вход: если A1B1==A2B2 && B1C1==B2C2 && C1A1==C2A2, то A1B1C1==A2B2C2

2. выход: тоже самое, но записанное в терминах аксиом Евклида.

emulek
()
Ответ на: комментарий от emulek

Память как раз принципиальна — в ФП она контекстная

Ну ты же понимаешь, что эта контекстная память - всего лишь сахар языка. Да, ты можешь накостылить, делов то. А проблема о которой ты, я так подозреваю, говоришь, заключается не в контекстной памяти, как таковой, а в том, что она неявная и недоступна для чтения записи в ЯП. Но это относится только к «чистым языкам», а я вот лично, не уверен, что чистота === функциональный подход.

anonimous
() автор топика
Ответ на: комментарий от emulek

Ну и какое это док-во? Это трансляция чистой воды и больше ничего. Все равно, что foo-->bar. Самого процесса доказательства я тут не вижу.

anonimous
() автор топика
Ответ на: комментарий от anonimous

Ну ты же понимаешь, что эта контекстная память - всего лишь сахар языка

ох... Вот это как раз суть языка.

Но это относится только к «чистым языкам», а я вот лично, не уверен, что чистота === функциональный подход.

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

emulek
()
Ответ на: комментарий от anonimous

Ну и какое это док-во? Это трансляция чистой воды и больше ничего. Все равно, что foo-->bar. Самого процесса доказательства я тут не вижу.

ты его не видишь потому, что мне лениво его выписывать. И программу мне лень писать, там Over9000 строк.

emulek
()
Ответ на: комментарий от emulek

Вот это как раз суть языка

Вот тут:

рекурсия и итерация (комментарий)

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

anonimous
() автор топика
Ответ на: комментарий от emulek

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

Геометрия евклида с точками и прямыми непротиворечива и существует как математическая конструкция.

cvs-255 ★★★★★
()
Последнее исправление: cvs-255 (всего исправлений: 1)
Ответ на: комментарий от anonimous

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

на мой пьяный(уже) взгляд, ты написал ||ню. Завтра посмотрю ещё раз...

emulek
()
Ответ на: комментарий от cvs-255

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

достаточно, но не необходимо.

Геометрия евклида с точками и прямыми непротиворечива и существует как математическая конструкция.

да. Это никак не доказывает её оторванность от RL. Она может быть и оторванной, и не оторванной. Ты утверждаешь, что она оторвана, а я — что нет.

emulek
()
Ответ на: комментарий от emulek

Ты как-то криво читаешь. Есть несколько (> 1) различных способов провести соответстиве между евклидовой геометрией и реальностью. О чем я и писал с самого начала.

cvs-255 ★★★★★
()
Вы не можете добавлять комментарии в эту тему. Тема перемещена в архив.