September 12th, 2021

Минимальная модель абстрактного универсального вычислителя и языка.

Минимальная модель абстрактного универсального вычислителя.
Минимальная модель абстрактного универсального языка.

Абстрактный универсальный вычислитель = ((ветвление) + (изменение памяти)).

Абстрактный универсальный вычислитель должен уметь делать:
1. ветвление (изменение порядка исполнения команд).
2. изменение памяти.

ps
Тьюринг-полнота компьютера с одной операцией.
https://deep-econom.livejournal.com/815663.html

pps (см. комменты к посту)
1. сравнения
2. ветвления
3. изменения памяти

ppps
Язык. Тотальный полиморфизм. Генезис любых языков.
https://deep-econom.livejournal.com/867415.html

книги для дошкольников

Сапгир, Луговская: Приключения Кубарика и Томатика, или Веселая математика
(2 части)

По следам Робинзона. Верзилин.
Физика на каждом шагу. Перельман.
Большая книга занимательных наук. Перельман.
Нескучная биология. Целлариус.
Элементарно! Вся таблица Менделеева у тебя дома. Майк Барфилд.
Как работает наука. Наглядные факты об устройстве нашего мира. Dorling Kindersley.
Как объяснить ребенку математику. Иллюстрированный справочник для родителей. Кэрол Вордерман.
Как объяснить ребенку науку. Иллюстрированный справочник для родителей по биологии, химии и физике. Кэрол Вордерман.
Программирование для детей. Иллюстрированное руководство по языкам Scratch и Python.

(no subject)

----
Сергей Бобровский
Кубическая теория типов для малышей

Вычислительная теория типов (Computational Type Theory, CTT) связывает конструктивную математику Мартина-Лёфа и программирование. CTT -- это теория конструктивной математики, основанная на вычислениях.

Конструктивная математика -- это математика, в которой мы манипулируем объектами конструктивно :) Нас интересуют не абстрактные характеристики со множеством деталей, а конкретные, прикладные в некотором смысле. Например, многие типы данных описываются через теорию множеств весьма сложно, а в конструктивном смысле нам достаточно иметь алгоритм (по Тьюрингу например), который бы формально, пусть и ограниченно, описывал некоторый тип. Кроме того, учитывается, что объекты не существуют вечно, а появляются и исчезают, и т. д. В конструктивной математике мы делаем большие допуски, большие послабления, жертвуя математической строгостью в пользу эффективной вычислимости. Во многих прикладных задачах нас вполне удовлетворит утиная типизация/абстракция отождествления (если что-то выглядит как утка и ходит как утка, то это скорее всего и есть утка), а те объекты, которые явно не похожи на утку, мы просто исключаем из рассмотрения.

Интуиционистская теория типов, например, построена на конструктивной математике. В Корнельском университете ещё с 1980-х годов разрабатывается система автоматических доказательств NuPRL, с её помощью удалось удачно формализовать ряд конструктивных теорий. Крутость NuPRL в том, что она исходит не из формальной системы типов, а из концепции программы, типы в которой -- характеристики её поведения. В результате удаётся сформировать очень богатую систему типов, охватывающую и типы в классическом смысле, и типы, завязанные на вычисления. И вот когда типы насыщаются семантикой, система автоматических доказательств становится очень прагматичной, ориентированной на реализацию, а не на абстрактные концепции.

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

Тут мы и подходим к зависимым типам, которые удобно трактовать именно в контексте вычислительной среды, языка программирования и понятия значения. "Прояснение смысла" определяет типы как программы, именующие спецификации поведения. Программы, которые ведут себя в соответствии со спецификацией, заданной типом, и будут считаться экземплярами этого типа. Ключевой момент такого прояснения -- это полная самопрояснённость в своих собственных терминах, абсолютно чёткая и однозначная. А попрактиковавшись в зависимых типах, дальше несложно уже будет и собственное мышление прояснять и рационально просветлять аналогичными формальными подходами.

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

Сегодня самый мировой топчик в развитии CTT -- это кубики, кубическая теория типов, Cubical Computational Type Theory (CCTT). Она расширяет CTT отождествлениями, или путями всех конечных измерений. Самые простые элементы типов имеют измерение 0. Элементы измерения n+1 -- это пути, которые связывают два элемента измерения n и свидетельствуют о взаимозаменяемости этих элементов во всех контекстах. Математически, тут связи с комбинаторной топологией и теорией категорий (точнее, теорией высших категорий [Лейнстер 2002] -- морфизмы морфизмов и вот это вот всё). С точки зрения программиста, такая структура высоких измерений по сути предлагает нам универсальный механизм симметричного(?) "приведения", преобразования типов друг в друга, который только в такой теории называется на casting, а coercion.

В сердце же всего этого -- гениальная аксиома унивалентности Воеводского:

эквивалентные (изоморфные, очень грубо) типы идентичны (взаимозаменяемы).
Как организовать такую структуру? Тут и было решено использовать кубики: типы и термы распределяются по слоям (измерениям), нулевое измерение соответствует стандартной CTT, и объект измерения n+1 будет n+1 - мерным кубом, который можно представить как связи между n-мерными кубиками -- n различными способами, соответствующими парам противоположных граней в каждом измерении. Например, трёхмерный кубик состоит из трёх пар противоположных граней -- двухмерных кубиков (квадратов). Применительно к программированию, кубик -- это программа, вычисление которой "чувствительно" к биндингу переменных доступных измерений, которые, двигаясь к 0 или 1 по своему измерению, индуцируют вычисление конечных точек линий, параметризованных этими переменными.

Наверное, ключевое в кубиках -- это сами линии типов (по которым бегают экземпляры типов в процессе тайпкастинга) и их конечные точки, которые подразумевают взаимозаменяемость типов подчас весьма сложным вычислительным образом. Далее, удалось формализовать понятие хорошо типизированных вычислений -- это те, которые когерентны в отношении порядка измерений (верхняя точка слева должна совпадать с левой точкой вверху). Наконец, линий типов должно быть достаточно, чтобы можно было строить нужные пути через их конкатенацию, ну и должны присутствовать линии более высоких измерений, чтобы обеспечить ассоциативность такой конкатенации. Тут ещё можно вспомнить условие Кана из теорката, переведённое на язык CTT -- результат должен вычисляться из спецификации задачи унифицированным способом.

Активно занимается этим Robert Harper из Карнеги-Меллона, входящий в дюжину святых Computer Science (развивает кубики, формализует ML, пишет самые крутые курсы CMU). Надеюсь, что какие-то кусочки его свежих лекций, пока их ещё можно достать в даркнете :) постепенно получится адаптировать к рациональному просветлению. Ну и попутно, попрактиковаться в тысячекратной компактности кода.

https://vk.com/@lambda_brain-cubical-computational-type-theory
---

(no subject)

Как правильно найти работу программером
(статья довольно длинная)

----
Сергей Бобровский
https://vk.com/wall-152484379_3417

Если вы программист, если вы учитесь на программиста, и у вас не очень хорошо получается, рассказываю, почему + что вам надо делать, чтобы начать наконец получать "от 150 000 до 500 000 Р" + также под катом инфа для тех, кто не умеет программировать, не знает с чего начать, как войти в ИТ, как заработать в ИТ если не хочешь/не можешь стать программистом, и т. п.

Сермяга в том, что если вы пытаетесь стать программистом, и обучение занимает у вас уже больше года, а вы ещё не докачались до уровня джуниора, или хотя бы стажёра, то, ну будем честны — скорее всего это не ваше. Обучение на профессию "программист" не должно занимать столько времени!

(продолжение по ссылке)
-----