На Хабре встречаются люди-цитаторы, которые любят какую-то идею или личное впечатление от статьи переносить в завуалированном виде (цитируя классиков), зачастую делают это без понимания материала статьи или без цели принести пользу
А электрический заряд? Не могу на ощупь отличить положительный от отрицательного.
Тут можно привести пример столкновения электрона и позитрона, которые несут положительный и отрицательный заряд и просто исчезают при столкновении, высвобождая энергию, которую можно почувствовать.
Но насколько это хороший пример - не знаю. Вообще, никакие числа нельзя пощупать в природе, но можно делать вычисления с их учетом и пощупать много-много применений этих вычислений.
Звучит, как интересная алгоритмическая задача, решаемая при глубоком понимании математической модели квантовых вычислений, а также предметной области ML. Но я не погружался в эту область, так как пока квантовые компьютеры сидят в очень узких лабораториях.
Если ML действительно будут запускать на квантовых компьютерах, то я 100% буду осваивать эту область. Но пока (насколько я понял) ML запускают на процессорах с архитектурой видеокарты типа NVIDIA, так что я бы скорее почитал про что-то типа CUDA
goto - это настолько плохо, что даже на уровне самих языков программирования его не стали добавлять. В Java его нет, например. Есть только очень узкий случай break LABEL; для выхода из многомерного цикла и все.
Мне - комфортно и с неконструктивной. Но комментатор выше написал "любые неконструктивные теоремы попросту бесполезны" и я пытаюсь понять, что имелось в виду
которые невозможно ни доказать, ни опровергнуть, ни даже понять.
Почему? В книге по теории типов, вполне четко объясняется параллель между теорией типов и реальной математикой, и дается конкретный пример теоремы Безу. И сама теория типов тоже довольно четко выстроена (на уровне метатеории).
Как быть с математическими объектами, состояние которых на определённой итерации в принципе непредсказуемо без вычисления предыдущих
Можете взять любой учебник по теории автоматов и ознакомиться. Игра жизни - это клеточный автомат. Отлично она формализуется, как и Машина Тьюринга. Они все довольно четко выражены в теории множеств. Трудность может быть только в том, чтобы конфигурацию машины Тьюринга в конкретный момент времени, и потом задать правило перехода от предыдущей к последующей
А можете раскрыть более подробно пункт про практическое применение конструктивной математики по сравнению с неконструктивной? Единственный пример что я знаю, это то, что из конструктивных доказательств можно потом в Coq синтезировать программы. Но если я доказываю всякие штуки из теории чисел, например? Какой там плюс?
Онлайн-библиотеки типа MML, смотреть\сравнивать можно
На Хабре встречаются люди-цитаторы, которые любят какую-то идею или личное впечатление от статьи переносить в завуалированном виде (цитируя классиков), зачастую делают это без понимания материала статьи или без цели принести пользу
Интересно, спасибо. Может стоит разобраться как это работает и вывести правила мат. логики полностью на комбинаторах
Я думаю, многие, кто взял кредит, ощущают на себе силу знака "минус" =)
Тут можно привести пример столкновения электрона и позитрона, которые несут положительный и отрицательный заряд и просто исчезают при столкновении, высвобождая энергию, которую можно почувствовать.
Но насколько это хороший пример - не знаю. Вообще, никакие числа нельзя пощупать в природе, но можно делать вычисления с их учетом и пощупать много-много применений этих вычислений.
Кстати, есть еще квантовая машина Тьюринга =)
Звучит, как интересная алгоритмическая задача, решаемая при глубоком понимании математической модели квантовых вычислений, а также предметной области ML. Но я не погружался в эту область, так как пока квантовые компьютеры сидят в очень узких лабораториях.
Если ML действительно будут запускать на квантовых компьютерах, то я 100% буду осваивать эту область. Но пока (насколько я понял) ML запускают на процессорах с архитектурой видеокарты типа NVIDIA, так что я бы скорее почитал про что-то типа CUDA
goto - это настолько плохо, что даже на уровне самих языков программирования его не стали добавлять. В Java его нет, например. Есть только очень узкий случай break LABEL; для выхода из многомерного цикла и все.
По моему опыту, 90% сайтов работает быстро и отзывчиво. Может это у вас старая ОС\железо или плохой интернет или роутер старый?
Мне - комфортно и с неконструктивной. Но комментатор выше написал "любые неконструктивные теоремы попросту бесполезны" и я пытаюсь понять, что имелось в виду
Обучение и развитие человека намного шире и может выходить за рамки того, что "учили".
Можно же обучаться самостоятельно (по книге или курсу), а также внутри IDE или симулятора. А еще можно проводить исследовательскую работу.
Почему? В книге по теории типов, вполне четко объясняется параллель между теорией типов и реальной математикой, и дается конкретный пример теоремы Безу. И сама теория типов тоже довольно четко выстроена (на уровне метатеории).
Можете взять любой учебник по теории автоматов и ознакомиться. Игра жизни - это клеточный автомат. Отлично она формализуется, как и Машина Тьюринга. Они все довольно четко выражены в теории множеств. Трудность может быть только в том, чтобы конфигурацию машины Тьюринга в конкретный момент времени, и потом задать правило перехода от предыдущей к последующей
Личный опыт и общение с такими людьми, а также чтение их статей и истории их жизни\карьеры
Ну вообще для DataScience-спецов держат, а это оно и есть
Хотелось бы разобраться, откуда это все следует
Я пытаюсь найти мотивацию, чтобы полностью отказаться от неконструктивной математики, но пока что не получается...
Интересно, спасибо
Может тут имеется в виду чистое программирование в любом виде или решение алгоритмических задач?
Интересно, зачем им Coq, они же "EX CORP. Мы создаем экосистему сервисов для игроков соревновательных игр"
Про аксиому выбора - да, все верно, она неконструктивна
А можете раскрыть более подробно пункт про практическое применение конструктивной математики по сравнению с неконструктивной? Единственный пример что я знаю, это то, что из конструктивных доказательств можно потом в Coq синтезировать программы. Но если я доказываю всякие штуки из теории чисел, например? Какой там плюс?