thedeemon: (Default)
[personal profile] 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 это означает, что если нам нужно реализовать например работу с матрицами, где нам придется умножать друг на друга число строк и столбцов, то для гарантирования корректности придется задействовать механизм конструктивных доказательств из прошлого поста.

Date: 2011-11-29 10:36 am (UTC)
From: (Anonymous)
Неразрешимость случая когда есть умножение следует, в том числе, из неразрешимости диофантовых уравнений.

Profile

thedeemon: (Default)
Dmitry Popov

May 2025

S M T W T F S
    123
45678910
11 121314151617
18192021222324
25262728293031

Most Popular Tags

Page Summary

Style Credit

Expand Cut Tags

No cut tags
Page generated Jul. 9th, 2025 12:11 am
Powered by Dreamwidth Studios