LINUX.ORG.RU

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

 ,


1

3

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

zvezdochiot ()

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Владимир

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

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

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

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

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

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

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

Как это?

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

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

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

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

Она одна.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

protsquest ()

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

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

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

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

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

Их две.

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

ZERG ★★★★ ()

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

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

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

anonymous ()

Владимир

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

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

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

anonymous ()