τ-lang: usage

Posted on January 10, 2020

Практика применения.

Рассмотрим сначала обвязку функций. Вот пример apply функции складывающей два натуральных числа:

Результат вызова: (S(S(S(S(S O)))))

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

Что здесь происходит? Объявляется функция у которой два параметра - a и b (складываемые числа), при этом телом функции является композиция функций (apply) в котором функцией является еще одно объявление функции: (sum a b => sum sum a b)

Вызов (3+2):

Рассмотрим код сортировки списка натуральных чисел:

    ( list =>
        (sort join filter lt ge list => sort sort join filter lt ge list)
        (sort join filter lt ge list =>
            match list
            | EMPTY => EMPTY
            | L head tail => join (sort sort join filter lt ge (filter tail (lt _ head)))
                                  (L head (sort sort join filter lt ge (filter tail ( ge _ head))))
        )
        (list1 list2 =>
            (join list1 list2 => join join list1 list2)
            ( join list1 list2 =>
                match list1
                | EMPTY => list2
                | L head tail => L head (join join tail list2)
            )
            list1
            list2
        )
        (list predicate =>
            ( filter filter' predicate list =>
                match list
                | EMPTY => EMPTY
                | L head tail => filter' ( filter filter filter' predicate tail ) head (predicate head) 
            )
            ( filter filter' predicate list =>
                match list
                | EMPTY => EMPTY
                | L head tail => filter' ( filter filter filter' predicate tail ) head (predicate head) 
            )
            ( list elem flag =>
                match flag
                | true => L elem list
                | false => list
            )
            predicate
            list
        )
        ( a b =>
            (lt lt' a b => lt lt lt' a b)
            ( lt lt' a b =>
                match b
                | O => false
                | S b' => lt' lt' lt a b'
            )
            (lt' lt a b' =>
                match a
                | O => true
                | S a' => lt lt lt' a' b'
            )
            a
            b
        )
        ( a b =>
            (ge ge' isZero a b => ge ge ge' isZero a b)
            ( ge ge' isZero a b =>
                match a
                | O => isZero b
                | S a' => ge' ge' ge isZero a' b
            )
            (ge' ge isZero a' b =>
                match b
                | O => true
                | S b' => ge ge ge' isZero a' b'
            )
            (x =>
                match x
                | O => true
                | S x' => false
            )
            a
            b
        )
        list
    )
    (L (S(S(S(O)))) (L (S(S(S(S(S(O)))))) (L (S(S(S(S(O))))) (L (S(S O)) EMPTY))))

Натуральные числа, тип boolean и списки мы задаем индуктивно, в синтаксисе Coq это выглядело бы так:


Inductive bool : Type :=
  | true
  | false.

Inductive nat : Type :=
  | O
  | S (n : nat).

Inductive list : Type :=
  | EMPTY
  | L (head : nat) (tail: list).

Мы рассматриваем τ-lang без типов, типы в синтаксисе Coq приведены для понимания структуры данных с которыми работает сортировка.


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

Нет, не так. Язык обладает Тьюринг полнотой, так как на нем можно написать модель машины Тьюринга. Кроме Тьюринг полноты есть еще одно свойство которое позволяет привести абсурдный пример с доказательством отсутствия оракула. То есть рефлексия, возможность модели изучать собственные свойства. Вооот! Тьюринг полнота + рефлексия. То есть если реализована Тьюринг полная модель - то там уже будет рефлексия. Интерпретатор Тьюринг полный, но модель самого интерпретатора - без рефлексии, то есть модели функций написанные на нем не имеют доступа к собственным свойствам. Что не мешает при их помощи написать модель машины Тьюринга с рефлексией и устроить абсурд на ней.


Интроспекция и рефлексия

весь код анализа можно написать на самом τ-lang. Есть два варианта - сделать замыкание (рефлексию) или проброс механики интерпретатора в язык (то есть получить доступ из языка к внутренним структурам интерпретатора) либо (более интересный вариант) - реализовать интерпретатор языка на нем самом и анализировать не программы написанные на τ-lang для собственно интерпретатора а программы написанные для модели интерпретатора написанного на τ-lang. При этом и сам интерпретатор и анализируемы программы и код анализ - все реализуемо на одном языке.

язык описания структуры

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

(S (S (S O)))

 S
  \
   S
    \
     S
      \
       O

Список - точно такая же структура, только каждый узел имеет кроме одного потомка еще и значение (в зависимости от типа списка). Вот пример списка чисел:

(L (S(S O)) (L (S O) EMPTY))

 L-[ (S(S O)) ]
  \
   L-[ (S O) ]
    \
     EMPTY

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