Войти в систему

Home
    - Создать дневник
    - Написать в дневник
       - Подробный режим

LJ.Rossia.org
    - Новости сайта
    - Общие настройки
    - Sitemap
    - Оплата
    - ljr-fif

Редактировать...
    - Настройки
    - Список друзей
    - Дневник
    - Картинки
    - Пароль
    - Вид дневника

Сообщества

Настроить S2

Помощь
    - Забыли пароль?
    - FAQ
    - Тех. поддержка



Пишет kouzdra ([info]kouzdra)
@ 2013-04-06 18:52:00
Previous Entry  Add to memories!  Tell a Friend!  Next Entry
9x2
Между прочим адептам коммутативности на заметку:

Возьмите в качестве примера аксиоматику Пеано (где никакой коммутативности кстати нет - там это доказывать надо) - сколько по вашему взрослых людей с высшим техническим это хотя бы знают (не говорю уж о "понимают")? Imho меньше 50%.

Ну или черчевские нумералы - это вообще между прочим у даже матстудентов "моментальный вынос мозга" как правило.

А теперь представьте себе что вы стали объяснять арифметику начиная с аксиоматики Пеано или лябмда-исчисления?

(Добавить комментарий)


[info]kaledin
2013-04-06 23:48 (ссылка)
Да кому это старье нахуй нужно?

Это вообще никогда не было математикой; просто Гильберт зарвался и захотел все на свете доказать, ему указали что нельзя, ок, все все поняли, вопрос закрыт. Нахуй надо помнить и знать сложные технические навороты для решения частной задачи, популярной еще до войны?

(Ответить) (Ветвь дискуссии)


[info]kouzdra
2013-04-06 23:54 (ссылка)
Если все эти задачи были бы никому не нужны - про них бы и не вспоминали.

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]kaledin
2013-04-07 00:07 (ссылка)
Про них вспоминают только потому, что история -- ах! -- драматическая, а формулировки -- увы -- можно обьяснить гуманитарию (он правда все равно не поймет, но обьяснить можно).

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]kouzdra
2013-04-07 00:12 (ссылка)
Да оператор фиксированной точки чуть не главное, что вообще есть...

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]kaledin
2013-04-07 00:45 (ссылка)
Не-не, я про арифметику Пеано, Goedel enumeration и пр. Ламбда-калкулус это другое.

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

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]kouzdra
2013-04-07 11:00 (ссылка)
На сам деле ничего особенного в лямбдах нет - это примерно тоже что декартово замкнутые категории или позитивные логики (отличия есть но скорее технические).

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

и Y тут важен не как проблема - а как ее решение - ну да - нормальная формальная семантика для самоприменимости.

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]kaledin
2013-04-07 13:20 (ссылка)
>это примерно тоже что декартово замкнутые категории

Нет не то же. Декартово замкнутые категории это полная банальность.

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]kouzdra
2013-04-07 13:26 (ссылка)
Так и лямбды - полная банальность. Очередной синтаксический формализм, довольно удачный но и не более. Просто так вышло, что в начале прошлого века автореферентности очень напугались и из теории множеств ее старательно вычистили - вопрос на засыпку - почему не может быть множества {x} = x)

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]kouzdra
2013-04-07 13:29 (ссылка)
PS: Лямбды от рекурсивных функций принципиально не отличаются - просто они проще - потому когда с этим реально стали работать - переползли на более простой формализм. Но в принципе это техника.

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]kaledin
2013-04-08 00:16 (ссылка)
Вот видно программиста. Для тебя эквивалентные определения эквивалентны. А мы типа бьемся в поте лица за удобные и концептуально правильные. Потому что память человеческая очень ограничена, увы.

(Ответить) (Уровень выше)


[info]dshtuk.livejournal.com
2013-04-07 11:21 (ссылка)
Ну не знаю... Арифметика Пеано - штука очень осмысленная. Особенно в смысле преподавания: простая базовая идея, на которой можно много всего построить, ту же математическую индукцию. Равно как и Геделевская нумерация. Да как хоть ту самую теорему доказывать, что "ничего не доказывается"? Руками махать? Или принять на веру?

Конечно, может, в дифф. геометрии оно и не очень нужно, но это частный вопрос.

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]kouzdra
2013-04-07 11:24 (ссылка)
Ты же из нее без индукции ничего не сделаешь. А с каким скрипом входит индукция - сам же знаешь.

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]dshtuk.livejournal.com
2013-04-07 15:36 (ссылка)
Так это и есть метод (по крайней мере у И.А.) объяснять индукцию. Они идут парой, неразрывно - индукция и аксиомы Пеано.

(Ответить) (Уровень выше)


[info]kaledin
2013-04-07 13:21 (ссылка)
>может, в дифф. геометрии оно и не очень нужно

Не только в "дифф. геометрии", а вообще в математике. Да и в логике -- которая не математика -- тоже старье неактуальное.

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]dshtuk.livejournal.com
2013-04-07 15:35 (ссылка)
А что на этом месте актуально? Выбросим основания математики на свалку истории? Не будем изучать т. Гёделя о неполноте?

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

(Ответить) (Уровень выше)


[info]potan
2013-04-09 12:18 (ссылка)
В системах типов аксиоматика Пиано возникает.

(Ответить) (Уровень выше)


[info]kouzdra
2013-04-09 12:27 (ссылка)
PS: На сам деле знать полезно как раз чтобы потом не тратить время на хуйню и изобретение велосипеда. Ну простая структура которая много где возникает.

Собственно смысл примерно как у таблицы умножения.

(Ответить) (Уровень выше)


[info]17ur.livejournal.com
2013-04-07 21:51 (ссылка)
Пеано - матиндукция? В школе подарили за районную матолимпиаду математический словарь, там это было...

(Ответить) (Ветвь дискуссии)


[info]kouzdra
2013-04-07 21:55 (ссылка)
Разумеется - оно чисто на этом - докажите хотя бы коммутативность сложения там.

(Ответить) (Уровень выше)