LINUX.ORG.RU

Логика и грамматика в программировании

 ,


1

3

Иногда встречаются утверждения, что формальная логика сводится к построению грамматически «корректного» языка, не допускающего противоречивых высказываний. Правда ли это?

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

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

Каково соотношение межуд логикой и формальной логикой? Что общего между ними?



Последнее исправление: protsquest (всего исправлений: 1)

Каково соотношение межуд логикой и формальной логикой? Что общего между ними?

Как кактус не назови, ёлкой не станет.

Всегда надо идти к источнику.

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

ЛОГИКА пляшет от смысла высказываний.

Где одно и где второе? И что общего?

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

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

Да, но предварительно текст программы может быть проверен на корректность

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

Да, но предварительно текст программы может быть проверен на корректность

Это не меняет ни суть проги, ни суть ЯП. Или меняет?

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

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

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

В этом, собственно и смысл формальной логики, насколько я понимаю

И всё это опять упирается в:

выполнение инструкций процессора

Шаг влево, вправо, прыжок на месте - попытка улететь.

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

Это не совсем по теме, я думаю. Там обсуждается вопрос возможности иметь полную систему не содержащую противоречий. Вопрос полноты я тут не поднимаю

protsquest
() автор топика

Иногда встречаются утверждения

Где встречаются? Нужны ссылки. Такое впечатление, что речь идёт не о языках программирования, а о языках формальной верификации (типа Coq).

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

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

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

Вы не согласны с этим утверждением?

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

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

Ну понять его не трудно. Есть некий язык который грамматически не допускает некорректных высказываний,как например выражение «верхний низ» или «1+1=3». Проверка грамматики таким образом, становится одновременно и проверкой корректности. В приведенных примерах грамматически верные выражения некорректны

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

не допускающего противоречивых высказываний

man теорема гёделя

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

Противоречивость: Возможно одновременно доказать X и !X Невыводимость: невозможно доказать X и невозможно доказать !X

Теорема Геделя утверждает, что в достаточно сложных системах аксиом существуют невыводимые формулы.

Crocodoom ★★★★★
()
Последнее исправление: Crocodoom (всего исправлений: 2)
Ответ на: комментарий от AndreyKl

Владимир

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

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

Невыводимость: невозможно доказать X и невозможно доказать !X

А в чем тут проблему кстати нашли? Невыводимую и неопровержимую формулу суешь в аксиомы и все.

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

Все не засунешь, сколько не старайся. Это напрямую следует из теоремы.

Доказательство: Допустим, мы засунули в систему аксиом все такие невыводимые формулы. Применим для этой системы теорему Геделя. Ч.Т.Д.

Crocodoom ★★★★★
()
Последнее исправление: Crocodoom (всего исправлений: 2)
Ответ на: комментарий от protsquest

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

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

Как это?

Он утверждает, что для некой системы, построенной, допустим, на 5-ти аксиомах, существует формула, которая невыводима и неопровержима в данной системе. Она одна. Но и любая аксиома является такой формулой. Таким образом у нас на выходе 6 аксиом, вот и все. Просто придаем этой формуле статус аксиомы. На количество аксиом ограничений нет

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

Насколько я знаю, да. Что то из логик низших порядков считаются такими

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

Он утверждает, что для некой системы, построенной, допустим, на 5-ти аксиомах, существует формула, которая невыводима и неопровержима в данной системе.

Для любой системы, содержащие эти «пять аксиом»

Она одна.

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

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

Доказательство: Допустим, мы засунули в систему аксиом все такие невыводимые формулы. Применим для этой системы теорему Геделя. Ч.Т.Д.

Это не доказательство а подлог. Если гипотеза не подтвердилась, нельзя ее подтвердить самоприменением

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

Там говорится о хотя бы одной, по-моему. Одна или более. Это не важно в данном случае. Засовываем в аксиоматику все эти формулы. Не важно сколько их

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

А как вам удается различать anonymous-ов?

Во-первых — стаж.

Во-вторых — вопрос хороший, непосредственно относящийся к теме обсуждения.

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

Это не доказательство а подлог.

Так программирование и есть подлог. Обработчик исключений - это кто?

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

Давай. Засунули. Получили новую систему аксиом. Для неё снова применяем теорему Геделя, и что получаем? :)

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

Это не доказательство а подлог. Если гипотеза не подтвердилась, нельзя ее подтвердить самоприменением

Бессмысленный набор слов

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

Для неё снова применяем теорему Геделя, и что получаем? :)

Засунув мы опровергаем гипотезу. Дальнейшее применение невозможно тут

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

выражение «верхний низ» или «1+1=3»

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

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

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

Приведенные примеры это выражения формального языка, который грамматически допускает противоречивые высказыания

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

А в чем тут проблему кстати нашли? Невыводимую и неопровержимую формулу суешь в аксиомы и все.

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

Проблема это или нет — зависит.

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

Пожалуйста, не провоцируй на применение выражений формального языка!

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

Гедель: я заявляю гипотезу, что любая богатая система если она непротиворечива, содержит формулу(ы), которая недоказуема и неопровержима[далее идет доказательство]

Оппонент: те формулы, которые ты обнаружил, являются аксиомами данной системы. Твоя гипотеза опровергнута

Гедель. Тогда для опровержения твоего контраргумента я применяю гипотезу, которую ты опроверг

protsquest
() автор топика

Это не соответствует понятию логики вообще, которая пляшет не от языка, а от смысла высказываний

Логика? От смысла? Ты где такую логику-то нашел?

Надеюсь, ты не про диалектику...

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

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

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

Теорема Геделя утверждает

Их две.

В несколько вольной трактовке можно сказать, что если система аксиом полна, то она противоречива, потому что ты можешь доказать утверждение А и утверждение !А.

ZERG ★★★★★
()

Каково соотношение межуд логикой и формальной логикой?

Если ты про Аристотеля, то прямое.

Если ты про Гегеля, то никакого соотношения, диалектика гегеля(равно как и диамат) - нечто вроде шизофазии.

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

Нет, я не про диамат

Какое именно прямое отношение?

protsquest
() автор топика

Владимир

Иногда встречаются утверждения, что формальная логика сводится к построению грамматически «корректного» языка, не допускающего противоречивых высказываний. Правда ли это?

Просьба привести URL /не понятно о чем речь/.

Упрощенно.
Обычно лексические анализаторы проверяют возможность вывода
анализируемого текста с использованием правил грамматики /и не более того/.

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

Ло́гика (др.-греч. λογική — «наука о правильном мышлении», «способность к рассуждению» от др.-греч. λόγος — «логос», «рассуждение», «мысль»

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