b
типы это “решение” парадокса рассела
Size: a a a
2020 October 29
p
что я имею в виду: стул или красный?
Зависит от контекста
b
который возникает в результате применения символизма фреге для описания формальных систем, таких как язык, например
b
я не хочу сейчас начинать про парадокс Рассела, просто ссылку приложу для тех кто не шарит https://ru.wikipedia.org/wiki/Парадокс_Рассела
p
Функция foo: a -> b говорит что если мы имеем объект типа а мы можем получить объект типа b
Аппликация foo 1 говорит "сделай foo с объектом 1"
b
грубо говоря этот пример про красный стул прекрасно иллюстрирует это свойство языка быть категорически нечетким, то есть мы не можем с уверенностью говорить про красный стул, как про красный или стул в каждом из использований красного стула в нашем языке
b
в чем здесь по–настоящему заключается неясность, неопределенность?
b
вы хотите перевести из одного языка в другой, причем чтобы в другом языке у вас получилась какая–то вычисляемая sound хуйня и хорошо кстати если она еще halting problem будет решать помимо всего прочего
b
ну то есть всегда можно собрать такой язык, который никакой переводчик не сможет перевести
b
вот эта типовая информация которую вы записываете при помощи типовых аннотаций, типовой структуры, комбинаторов и т.д. это все по сути инструкции по тому, какую логическую форму нужно собрать на компьютере
b
вопрос: кто вам сказал что нельзя эту информацию записывать не явным образом как часть структуры текста, а выделить ее в интерпретацию текста, а все необходимые инструкции “закодировать” в трансформер?
b
революционная идея? да. что невозможного? ничего
p
Трансформер кодируется целыми днями
s
Напомню, что язык машины это переписывание символов в символы.
s
Это единственное, что умеют делать тьюринг-полные вычислители.
b
в этом и есть диалектов в логосе. результатом парсинга диалекта в логосе является набор грамматик, которые фидятся в duct–программу и она на основе своего представления о том, как подобные грамматики могут использоваться, строит представление о том, как это использование может отражать определенную логическую форму. deduct программа, в свою очередь, выполняет обратную работу.
p
Трансформер кодируется целыми днями
Поэтому для типовых задач он может хорошо заработать, а для нетиповых он не будет адекватным решением
b
Напомню, что язык машины это переписывание символов в символы.
да но есть определенные переписывания которые линейно и гиперлинейно масштабируются
b
например ты можешь n^3 умножения матриц делать за 1/k*O(n^2.7) где k=1000000 охулион нулей
b
то есть гипотетически какая–то проблема, сложность которой в классическом поисковом дереве была бы космическая, можно делать значительно быстрее, чем кажется.