Фундаментальная математика — теория всего в IT и не только. Теория типов и формализация в Coq
У нас есть 3 "теории всего" - научная картина мира (все сводится к законам физики), информатика (все сводится к битам) и фундамент математики (все сводится к логике). Именно фундамент математики представляет особый интерес, так как он является фундаментом для двух других фундаментов и имеет глубокий философский смысл. Последние 2 года я сильно им увлекся и проделал довольно большую работу по углубленному изучению теории типов (Calculus of Constructions), и готов поделиться результатами, а также рассказать о девяти направлениях, где можно применить это на практике. Очень многое получилось лучше, чем я планировал. Изначально перспективы были не очень понятными, и поэтому я не рассказывал друзьям и коллегам про мою работу в этом направлении и называл это "Секретный Проект". Но теперь, когда многое прояснилось и получилось, можно поделиться успехом. Собственно, в этой статье я расскажу вам не только про сам фундамент математики, а еще его связь с ежедневной работой программиста, а также с Computer Science/Data Science и AI/ML. Я вам нарисую большую и красивую картину, на которой все понятно и логически следует из маленького набора правил выведений типов (11 штук) и аксиом теории множеств (9 штук).
У нас есть 3 фундамента математики - теория множеств (удобна для человека), теория типов (удобна для компьютера) и теория категорий (не знаю, зачем она вообще нужна). Они примерно одинаковой мощности и одну можно выразить внутри другой. Особый интерс представляет именно теория типов, тк ее довольно легко можно запрограммировать внутри компьютера и использовать как строгий фундамент для других теорий, который не дает совершить ошибку и проверяет каждое ваше действие.
Читать далее
#calculus_of_constructions #coq #type_theory #lambda_calculus #theorem_prover #фундамент_знаний #фундамент_математики #zfc | @habr_ai
У нас есть 3 "теории всего" - научная картина мира (все сводится к законам физики), информатика (все сводится к битам) и фундамент математики (все сводится к логике). Именно фундамент математики представляет особый интерес, так как он является фундаментом для двух других фундаментов и имеет глубокий философский смысл. Последние 2 года я сильно им увлекся и проделал довольно большую работу по углубленному изучению теории типов (Calculus of Constructions), и готов поделиться результатами, а также рассказать о девяти направлениях, где можно применить это на практике. Очень многое получилось лучше, чем я планировал. Изначально перспективы были не очень понятными, и поэтому я не рассказывал друзьям и коллегам про мою работу в этом направлении и называл это "Секретный Проект". Но теперь, когда многое прояснилось и получилось, можно поделиться успехом. Собственно, в этой статье я расскажу вам не только про сам фундамент математики, а еще его связь с ежедневной работой программиста, а также с Computer Science/Data Science и AI/ML. Я вам нарисую большую и красивую картину, на которой все понятно и логически следует из маленького набора правил выведений типов (11 штук) и аксиом теории множеств (9 штук).
У нас есть 3 фундамента математики - теория множеств (удобна для человека), теория типов (удобна для компьютера) и теория категорий (не знаю, зачем она вообще нужна). Они примерно одинаковой мощности и одну можно выразить внутри другой. Особый интерс представляет именно теория типов, тк ее довольно легко можно запрограммировать внутри компьютера и использовать как строгий фундамент для других теорий, который не дает совершить ошибку и проверяет каждое ваше действие.
Читать далее
#calculus_of_constructions #coq #type_theory #lambda_calculus #theorem_prover #фундамент_знаний #фундамент_математики #zfc | @habr_ai
Хабр
Фундаментальная математика — теория всего в IT и не только. Теория типов и формализация в Coq
У нас есть 3 «теории всего» — научная картина мира (все сводится к законам физики), информатика (все сводится к битам) и фундамент математики (все сводится к логике)....
Serverless tensorflow на AWS Lambda
Машинное обучение и нейросети становятся все более незаменимыми для многих компаний. Одна из основных проблем, с которыми они сталкиваются — деплой такого рода приложений. Я хочу показать показать практичный и удобный способ подобного деплоя, для которого не требуется быть специалистом в облачных технологиях и кластерах. Для этого мы будем использовать serverless инфраструктуру. Читать дальше →
#aws #lambda #tensorflow #serverless #deep_learning #machine_learning #глубокое_обучение #машинное_обучение #faas | @habr_ai
Машинное обучение и нейросети становятся все более незаменимыми для многих компаний. Одна из основных проблем, с которыми они сталкиваются — деплой такого рода приложений. Я хочу показать показать практичный и удобный способ подобного деплоя, для которого не требуется быть специалистом в облачных технологиях и кластерах. Для этого мы будем использовать serverless инфраструктуру. Читать дальше →
#aws #lambda #tensorflow #serverless #deep_learning #machine_learning #глубокое_обучение #машинное_обучение #faas | @habr_ai
Хабр
Serverless tensorflow на AWS Lambda
Машинное обучение и нейросети становятся все более незаменимыми для многих компаний. Одна из основных проблем, с которыми они сталкиваются — деплой такого рода приложений. Я хочу показать показать...