τ-lang: prerequisites

Posted on January 13, 2020

Здесь краткое и довольно поверхностное объяснение основных терминов и абстракций. Если Вы понимаете что такое constructor ground terms, индуктивные типы, почему (S (S (S O))) == 3, читали труды Черча и Клини в оригинале - то можете переходить к следующей статье, тут для Вас ничего особо интересного скорее всего не будет.

Ниже изложено краткое описание терминов, чисто mental model, достаточный для понимания τ-lang и τ2. Никаких фундаментальных основ, если Вам нужна крепкая теория - внизу есть список литературы.
  • моделирование

    Первая и самая важная мысль с которой придется столкнуться не раз. Мы работаем с моделями. Мы не знаем что такое число - это какая то абстракция, мы определили для нее операции, но по сути мы не знаем что это такое. У числа нет длины, высоты, массы, запаха, нет внутренней структуры, это что то единое, неделимое и, наиболее важное - несуществующее в природе. То что мы называем числами, пишем на бумаге, используем в научных трудах - это все МОДЕЛИ чисел. Число разрядов - это свойство модели а не самого числа. 810 и 10002 это одно и тоже число, отличается лишь форма записи. Эта самая форма и есть представление модели. А вот делимость на два - это свойство самого числа и не меняется от модели к модели. Конечность или бесконечность дроби - это свойство модели, а вот рациональность/иррациональность - это свойство числа. И так далее. Нам очень часто придется это учитывать, поэтому я рекомендую поиграть с этой мыслью. Глубже в мысль можно погрузиться в теории моделей, но для дальнейшего понимания τ-lang это совершенно не обязательно.

    Развивая мысль дальше можно понять что то же самое справедливо и для функций. Функция - это абстракция, она не существует во времени, у нее нет runtime и свойства завершаемости. A то что мы записываем в виде кода или в λ-нотации - это внезапно модель функции.

    Функции в программировании являются моделями функций в математическом значении (в дальнейшем под словом функция я подразумеваю абстрактное математическое понятие). Наиболее важным свойством модели отсутствующим у функции является разнесенность во времени. У модели при вычислении результата можно выделить начало вычислений, процесс вычислений, возврат результата. У функции нет до или после - мы применяем функцию к какому либо значению из области определения и получаем результат из области значений. Это атомарная операция, нет ни до ни после ни во время.

    Это наблюдение имеет важное следствие - halting problem не является проблемой функции, это проблема модели. Если у нас есть функция и значение из области определения - мы всегда получим значение из области значений. Для функции может быть проблемой выразить область определения/значений, но это совсем другая проблема. Таким образом пытаясь так или иначе решить halting problem мы всегда анализируем модели функций, причем анализируем именно собственные свойства этих моделей (точнее будет сказать - мы анализируем модели и пытаемся понять моделями чего они являются, так как не все модели моделируют функции).

    Собственно пока все о моделировании.

  • индуктивные типы
  • constructor ground term
  • pattern matching
  • композиция функций
  • partial apply и carrying
  • полиморфизм