Формальные теории

[Евгений Машеров]

bootstrap.
В программистском смысле, в статистическом другое значение слова.
Запуск программы делает программа, кто запускает первую программу?
Ответ в том, что есть некая простейшая, аппаратно реализованная, возможно, крайне примитивная и бедная по возможностям, и способная лишь из фиксированного места загрузить фиксированное число байт в фиксированный адрес памяти и передать управление. А то, что загружено - куда более богатая программа, которая загружает более сложную, пока не дойдём до полноценной ОС, загружающей пользовательский софт.
Применительно к данной проблеме - теорию мы описывает в терминах теории, как описать первую теорию?
Ответ в том, что "самая первая" теория примитивна и неформализована. Её можно выразить в терминах более сложных теорий, но это излишне. Скажем, совокупность символов, интуитивно, на бытовом уровне понятно, что это несколько символов, записанных в определённом порядке. Можно назвать "множеством", но у множеств есть определённые свойства, операции и пр., и выражать словами "множество" будет либо вульгаризацией (потому, что для совокупности свойства множеств не определены), либо строго, но переусложено. И, используя эти "строительные леса", вводим более сложные конструкции. В которых уже надобность в "интуитивной понятности" отпадает, первичные понятия определены и с ними оперируют по строгим правилам. И так доходят до сложных конструкций.

[Rasool]

Евгений Машеров в сообщении #1300523 писал(а):

bootstrap.
Ответ в том, что "самая первая" теория примитивна и неформализована. Её можно выразить в терминах более сложных теорий, но это излишне. Скажем, совокупность символов, интуитивно, на бытовом уровне понятно, что это несколько символов, записанных в определённом порядке. Можно назвать "множеством", но у множеств есть определённые свойства, операции и пр., и выражать словами "множество" будет либо вульгаризацией (потому, что для совокупности свойства множеств не определены), либо строго, но переусложено. И, используя эти "строительные леса", вводим более сложные конструкции. В которых уже надобность в "интуитивной понятности" отпадает, первичные понятия определены и с ними оперируют по строгим правилам. И так доходят до сложных конструкций.

Резюмируя: что было в начале - курица или яйцо?

[arseniiv]

(Оффтоп)

Не стоит так «резюмировать». Если бы в нашем языке было слово для генерализованной проблемы, можно было бы «дорезюмировать» до него, и какой толк?

[Dmitriy40]

(Курица или яйцо?)

Rasool в сообщении #1300546 писал(а):

Резюмируя: что было в начале - курица или яйцо?

Не удержусь и приведу ответ:

[beroal]

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

epros в сообщении #1300407 писал(а):

SomePupil в сообщении #1300361

wrote:
Преподаватель ответила "про совокупности символов". Я переспросил: "Значит, все-таки про множества символов?" После нескольких итераций преподаватель невольно согласилась, что говорится о множествах. Я бы сказал: "о строках символов".

SomePupil в сообщении #1300361 писал(а):

Потом зашла речь про правила вывода. Оказывается, это отношения, заданные на формулах.

Эти отношения обычно бесконечны, поэтому в начальной теории их быть не может. В начальной теории правило вывода есть список вида (следствие, список посылок). Следствия и посылки — это формулы. С помощью правил вывода проверяется правильность вывода.

В целом для начальной теории достаточно конечных множеств, списков и конечных деревьев. Формулы — это списки символов, выводы (доказательства) — деревья. В принципе, можно сказать, что формулы — это деревья, да и доказательства оформить в виде списков символов, но традиционно так, как выше.

[arseniiv]

beroal в сообщении #1300582 писал(а):

В начальной теории правило вывода есть список вида (следствие, список посылок). Следствия и посылки — это формулы.

Если вы хотите так сделать, придётся использовать ещё специальные переменные для формул и многие другие вещи (для указания ограничений). В результате тогда проще сказать, что правило вывода — это всюду определённая вычислимая функция из некоторого набора формул в истинностное значение (например).

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

[Sicker]

Dmitriy40 в сообщении #1300549 писал(а):

Не удержусь и приведу ответ:

У вас немного устаревшее дерево Черепахи должны быть немного раньше крокодилов.

[Dmitriy40]

Как видно из подписи на картинке, это не у меня. И на существо вопроса никак не влияет.

[Sicker]

Dmitriy40 в сообщении #1300601 писал(а):

Как видно из подписи на картинке, это не у меня. И на существо вопроса никак не влияет.

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

[Anton_Peplov]

(Курица и яйцо)

1. Прийти в тему.
2. Не сказать ничего онтопного.
3. Придраться к оффтопной, но смешной шутке с нерелевантными ей претензиями.
4. Не остановиться на одном сообщении и продолжить занудствовать.
Всегда так делаю. Я не прав?

[Chifu]

Евгений Машеров в сообщении #1300523 писал(а):

... Запуск программы делает программа, кто запускает первую программу? ...

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

[arseniiv]

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

-- Сб мар 31, 2018 18:11:52 --

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

[Chifu]

arseniiv в сообщении #1300702 писал(а):

Ничего не более естественные. ...

Сравнили метод развертывания от естественного языка до формальных систем и от машинного языка до прикладных программ. Мне представляется, что машинный язык является более формальным, а прикладные программы более естественные. Поэтому в процессе развертывания в первом случае формальность увеличивается, а во втором случае уменьшается.
Заметки:
1. Требуется время изучения программирования (как низкоуровневого, так и высокоуровневого, а желательно изучение их вместе).
2. Способ производства не важен - признак формальности.
3. Спецификации отражают программно-аппаратную организацию, соответственно отражают и степень формальности описываемого уровня. Отклонение от спецификации являются либо ошибкой спецификации, либо неиправностью вычислительного комплекса.
4. Возможность работы пользователя в прикладной программе на языке прикладной задачи, приближение к пользователю - признак естествености. Сами же задачи могут быть разного уровня формальности.
5. Под близостью к человеку понимается отсутствие необходимости разбираться в низкоуровневом устройстве.

[arseniiv]

А, так вы имеете в виду не языки, на которых пишутся программы, а «языки» интерфейсов этих программ, на которых с ними «говорит» пользователь (в основном что-то там нажимая мышкой). Ну, тогда возможно, вот только связь с темой немного уменьшается.