Entries by category: наука
По семь индексов да со штрихами на одной переменной. По-моему, это рекорд. Во всяком случае из того, что видел за последнее время:
Это Хокинг расстарался в свое время.
Это Хокинг расстарался в свое время.
Замечательный диалог тут вышел с моим любимым Шоном Кэрроллом (14 минут видео):
https://www.closertotruth.com/series/physics-consciousness
Про сознание, корабль Тесея, его копирование, зомби и стоит ли мечтать об аплоаде сознания в сеть (спойлер: видимо, не стоит).
Кэрролл еще раньше высказывался, что в физике нет места сознанию, что вот мол есть уравнения стандартной модели и они отлично описывают все физические процессы, и если бы было что-то нематериальное/духовное, что могло бы как-то влиять на физический мир (шевелить вашими мускулами, например), то это бы прямо противоречило экспериментальным проверкам текущих физических теорий. А здесь рядом David Chalmers явно указывает, где именно сознание может в физике прятаться - грубо говоря, в редукции волновой функции. О том же говорил и Менский у Гордона, и многие другие вплоть до чуть ли не Шрёдингера. Хороших ответов ни у кого пока нет, но есть о чем поразмыслить.
https://www.closertotruth.com/series/physics-consciousness
Про сознание, корабль Тесея, его копирование, зомби и стоит ли мечтать об аплоаде сознания в сеть (спойлер: видимо, не стоит).
Кэрролл еще раньше высказывался, что в физике нет места сознанию, что вот мол есть уравнения стандартной модели и они отлично описывают все физические процессы, и если бы было что-то нематериальное/духовное, что могло бы как-то влиять на физический мир (шевелить вашими мускулами, например), то это бы прямо противоречило экспериментальным проверкам текущих физических теорий. А здесь рядом David Chalmers явно указывает, где именно сознание может в физике прятаться - грубо говоря, в редукции волновой функции. О том же говорил и Менский у Гордона, и многие другие вплоть до чуть ли не Шрёдингера. Хороших ответов ни у кого пока нет, но есть о чем поразмыслить.
(Disclaimer: не то чтобы я в этом что-то понимал, будьте готовы к куче неточностей и ошибок)
Итак, допустим, ваш ребенок приходит из школы в слезах и говорит, что учитель зачеркнул 9*2 и вписал 2*9, "но ведь это одно и то же!"
А вы, будучи подкованы в современных веяниях науки, отвечаете так. Математика - это лишь прикладная теория типов, поэтому данный вопрос стоит рассмотреть с точки зрения этой теории. В теории типов у нас есть базовые суждения вроде "нечто является типом", "нечто является термом (выражением)" и "такой-то терм имеет такой-то тип" ("a : A"). Потом возникают индуктивные определения, состоящие из посылок и заключений. Например, "если A тип и В тип, то A -> B тоже тип". Еще: "если терм f имеет тип A -> B и терм x имеет тип A, то f x - это валидный терм, и он имеет тип В". Вводятся разные способы построения типов и термов: функция, произведение, сумма... Вводятся базовые типы. И вот тут первый ключевой момент. Если у нас есть терм
mul : Nat -> Nat -> Nat
то
mul 9 2 : Nat
Т.е. терм mul 9 2 - полноправный элемент типа Nat. Не число в привычной нам форме, не результат вычисления функции mul, а само выражение. Кажется, в этом одно из отличий типов от множеств. Никто не скажет, что выражение 9*2 входит в множество натуральных чисел, а вот в тип натуральных оно входит. И терм mul 2 9 тоже имеет тип Nat, и всякому очевидно, что mul 9 2 и mul 2 9 - это разные термы. А еще есть терм 18 того же типа, он на них совсем не похож, но все трое как-то связаны, они "равны". Что это значит? ( Read more...Collapse )
Итак, допустим, ваш ребенок приходит из школы в слезах и говорит, что учитель зачеркнул 9*2 и вписал 2*9, "но ведь это одно и то же!"
А вы, будучи подкованы в современных веяниях науки, отвечаете так. Математика - это лишь прикладная теория типов, поэтому данный вопрос стоит рассмотреть с точки зрения этой теории. В теории типов у нас есть базовые суждения вроде "нечто является типом", "нечто является термом (выражением)" и "такой-то терм имеет такой-то тип" ("a : A"). Потом возникают индуктивные определения, состоящие из посылок и заключений. Например, "если A тип и В тип, то A -> B тоже тип". Еще: "если терм f имеет тип A -> B и терм x имеет тип A, то f x - это валидный терм, и он имеет тип В". Вводятся разные способы построения типов и термов: функция, произведение, сумма... Вводятся базовые типы. И вот тут первый ключевой момент. Если у нас есть терм
mul : Nat -> Nat -> Nat
то
mul 9 2 : Nat
Т.е. терм mul 9 2 - полноправный элемент типа Nat. Не число в привычной нам форме, не результат вычисления функции mul, а само выражение. Кажется, в этом одно из отличий типов от множеств. Никто не скажет, что выражение 9*2 входит в множество натуральных чисел, а вот в тип натуральных оно входит. И терм mul 2 9 тоже имеет тип Nat, и всякому очевидно, что mul 9 2 и mul 2 9 - это разные термы. А еще есть терм 18 того же типа, он на них совсем не похож, но все трое как-то связаны, они "равны". Что это значит? ( Read more...Collapse )
