ATS и арифметика в типах

[thedeemon]

Сегодня тема попроще.

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

fn search {n,m:nat | m <= n}
  (str : string n, sub : string m) : [p:int | p <= n - m] int p = let
  val n = int1_of_size1 (string_length str)
  val m = int1_of_size1 (string_length sub)
  fun cmp {i,j:nat | i < n-m; j <= m} .<m-j>. 
    (i : int i, j : int j) :<cloref0> bool = 
      if j = m then true 
      else if str[i+j] = sub[j] then cmp(i, j+1) else false
    
  fun search_loop {k:nat | k <= n-m} .<n-k>. 
    (k : int k):<cloref0> [r:int | r <= n-m] int r = 
      if cmp(k, 0) then k 
      else if k < n - m then search_loop(k+1) else ~1
in
  if m <= n then search_loop(0) else ~1
end

Видите ошибку?
Что делает компилятор. Он выписывает указанные неравенства:

{ m <= n; i < n-m; j <= m; k <= n-m}

Плюс диктуемые определением nat:

{0 <= n; 0 <= m; 0 <= i; 0 <= j; 0 <= k; }

И начинает избавляться от переменных одну за одной. Берем переменную m, выписываем все, что меньше нее, все, что больше нее, и все, что ее не упоминает:

{ j <= m; 0 <= m;    m <= n; m < n-i; m <= n-k;    0 <= i ... }

Очевидно все, что меньше чем m, также меньше чем то, что больше m. Имея А выражений, которые меньше m, и B выражений, которые больше m, можно сформулировать A*B неравенств, которые их связывают, а переменную m выкинуть.

{ j <= n; j < n-i; j <= n-k;   0 <= n; 0 < n-i; 0 <= n-k;   0 <= i ...}

Теперь берем следующую переменную - i. Записываем все, что меньше, все, что больше, и остальное:

{ 0 <= i; j-n < i;    i < n;   j <= n; j <= n-k; 0 <= n; 0 <= n-k ...}

Избавляемся от i.

{ 0 < n; j-n < n; j <= n;    j <= n-k; 0 <= n; 0 <= n-k; ...}

И вдруг получили одновременно 0 < n и 0 <= n. Это противоречие: мы указали, что все должно работать для произвольного n >= 0, а выясняется, что для 0 система неравенств не выполняется. Ошибка! На самом деле компилятор ATS достаточно умен, чтобы указать на источник ошибки - неравенство i < n-m. Если его заменить на i <= n-m, то все компилируется успешно, все неравенства выполнимы.
Данный незамысловатый и полностью автоматизируемый процесс определения разрешимости системы неравеств путем последовательного избавления от переменных носит название Fourier–Motzkin elimination. Он гарантированно завершается, хоть и имеет нехилую сложность (дважды экспоненциальную). При каких условиях он работает? Когда все выражения линейны - состоят из сложений, вычитаний и умножений на константу. Как мне недавно подсказали, это арифметика Пресбургера. Как только появляется умножение переменных друг на друга или на себя, этот метод уже неприменим. Более того, было доказано, что теория первого порядка из натуральных чисел со сложением, умножением и равенством неразрешима, для нее универсального решающего алгоритма быть не может, иначе бы решалась проблема останова. См. Entscheidungsproblem. Для ATS это означает, что если нам нужно реализовать например работу с матрицами, где нам придется умножать друг на друга число строк и столбцов, то для гарантирования корректности придется задействовать механизм конструктивных доказательств из прошлого поста.

Comments

[diam-2003.livejournal.com]

А ещё кроме "работы с матрицами" в боевой практике встречается богомерзская косвенная адресация...

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

Это, конечно, не умаляет достоинств ATS как языка, демонстрирующего мосчь "доказательного программирования" на примерах, доступных для современного уровня развития технологии.

[(Anonymous)]

Неразрешимость случая когда есть умножение следует, в том числе, из неразрешимости диофантовых уравнений.

[si14.livejournal.com]

Интересно, правильно ли я понимаю, что какая-нибудь Agda, в отличие от ATS, умеет ограничено выводить доказательства сама даже в случаях с умножениями?

[thedeemon.livejournal.com]

В тред призывается nivanych! :)

[nivanych.livejournal.com]

Вроде, permea_kra поболее возился с агдой и его призывать более уместно.

[diam-2003.livejournal.com]

Agda может всё, для чего можно выписать алгоритм доказательства. В этом смысле она мощнее ATS. Есть ли там в библиотеках что-то кроме классики (Пресбургер, "хорошие" временные логики, политопы, ...) - не знаю.

[nivanych.livejournal.com]

Умеет, умеет. Только заметно ограниченно...
Старается как-то, и даже что-то получается.
Только даже для простых доказательств, порой, выводит такие простыни...

[madf.livejournal.com]

"... позволяют связать логически связать..." - одно "связать" лишнее.
Спасибо за интересный цикл!

[thedeemon.livejournal.com]

поправил, спасибо!