А вот интересно, есть ли фазовый переход при увеличении времени раздумий?

Эйнштейн говорил, что всё, что он делал, это оставался с интересными задачами дольше других.

Портия планирует нападение на добычу большего, чем она веса и размера и, наверное, ума, с помощью мозга в десять раз меньшего, чем у таракана. Она очень долго думает, однако ( Read more... )

Предсказуемость у нас двух видов - времени и качества ( Read more... )

У обычных векторов типы элементов не зависят от позиции. Это просто вектора, вектора векторов (матрицы) и тп.

Но можно определить вектор, у которого тип элемента от позиции зависит:
data DVec {n : Nat} {e : Nat -> Set} : Set1 where ( Read more... )

Для определения совпадений графов потоков данных необходимо сделать унификацию. С учетом того, что (a+b) унифицируется с (b+a).

Это, практически, последняя проблема.

Думаю, надо делать ее на бэктрекинге, но, пока, не понял как его лучше организовать. Без коммутативности такой проблемы бы не возникло. А где бэктрекинг - там и монады. ;)