Из Википедии, бесплатной энциклопедии
Перейти к навигации Перейти к поиску

В информатике , корекурсия является тип операции , которая является двойной к рекурсии . В то время как рекурсия работает аналитически, начиная с данных дальше от базового случая и разбивая их на более мелкие данные и повторяя до тех пор, пока не будет достигнут базовый случай, corecursion работает синтетически, начиная с базового случая и наращивая его, итеративно производя данные, удаленные из базовый вариант. Проще говоря, базовые алгоритмы используют данные, которые они сами производят, бит за битом, по мере того, как они становятся доступными и необходимыми, для получения дополнительных битов данных. Похожая, но отличная от других концепция - это генеративная рекурсия, в которой может отсутствовать определенное «направление», присущее коркурсии и рекурсии.

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

Corecursion может создавать как конечные, так и бесконечные структуры данных в качестве результатов и может использовать самодостаточные структуры данных. Corecursion часто используется в сочетании с ленивым вычислением , чтобы создать только конечное подмножество потенциально бесконечной структуры (вместо того, чтобы пытаться создать всю бесконечную структуру сразу). Corecursion - это особенно важная концепция в функциональном программировании , где corecursion и codata позволяют всем языкам работать с бесконечными структурами данных.

Примеры [ править ]

Corecursion можно понять по контрасту с рекурсией, которая более знакома. Хотя corecursion в первую очередь представляет интерес для функционального программирования, его можно проиллюстрировать с помощью императивного программирования, которое ниже выполняется с помощью средства генератора в Python. В этих примерах используются локальные переменные и присваиваются значения.императивно (деструктивно), хотя это не обязательно в corecursion в чисто функциональном программировании. В чистом функциональном программировании, вместо того, чтобы присваиваться локальным переменным, эти вычисленные значения образуют неизменяемую последовательность, а доступ к предыдущим значениям осуществляется путем самосылки (более поздние значения в последовательности ссылаются на более ранние значения в последовательности, которая должна вычисляться). Назначения просто выражают это в императивной парадигме и явно указывают, где происходят вычисления, что помогает прояснить изложение.

Факториал [ править ]

Классический пример рекурсии - вычисление факториала , который рекурсивно определяется как 0! : = 1 и n! : = n × (n - 1)! .

Чтобы рекурсивно вычислить свой результат на заданном входе, рекурсивная функция вызывает (копию) себя с другим (в некотором роде "меньшим") входом и использует результат этого вызова для построения своего результата. Рекурсивный вызов делает то же самое, если не достигнут базовый случай . Таким образом, в процессе создается стек вызовов . Например, для вычисления fac (3) это рекурсивно вызывает, в свою очередь, fac (2) , fac (1) , fac (0) ("свертывание" стека), после чего рекурсия завершается с fac (0) = 1., а затем стек раскручивается в обратном порядке, и результаты вычисляются на обратном пути по стеку вызовов к начальному кадру вызова fac (3), который использует результат fac (2) = 2 для вычисления окончательного результата как 3 × 2 = 3 × fac (2) =: fac (3) и, наконец, вернуть fac (3) = 6 . В этом примере функция возвращает единственное значение.

Это раскручивание стека может быть объяснено, определяя факториал corecursively , как итератор , где один начинается со случая , затем из этого начального значения строятся значения факториала для увеличения чисел 1, 2, 3 ... как в приведенном выше рекурсивном определении с "стрела времени" как бы перевернутая, прочитав ее в обратном направлении как . Corecursive алгоритм , таким образом , определяется производит поток из всех факториалов. Это может быть конкретно реализовано как генератор . Символически, отмечая, что вычисление следующего факториала требует отслеживания как n, так и f (предыдущее факториальное значение), это можно представить как:

или в Haskell ,

 ( \ ( П , е )  ->  ( п + 1 ,  е * ( п + 1 )))  ` итерация `  ( 0 , 1 )

это означает, что "начиная с , на каждом шаге следующие значения вычисляются как ". Это математически эквивалентно и почти идентичен рекурсивное определение, но подчеркивает , что факторные значения строятся вверх , идя вперед из исходного случая, а не вычисляются после первой иду в обратном направлении, вниз к основанию случае с декрементом. Прямой вывод функции corecursive не просто содержит факториальные значения, но также включает для каждого значения вспомогательные данные его индекса n в последовательности, так что любой конкретный результат может быть выбран среди них всех, когда и когда это необходимо.

Существует связь с денотационной семантикой , где обозначения рекурсивных программ выстраиваются таким образом коркурсивно.

В Python рекурсивная факториальная функция может быть определена как: [a]

def  factorial ( n ):  "" "Рекурсивная факториальная функция." ""  if  n  ==  0 :  return  1  else :  return  n  *  factorial ( n  -  1 )

Затем это можно было бы вызвать, например, factorial(5)для вычисления 5! .

Соответствующий коркурсивный генератор можно определить как:

def  factorials ():  "" "Corecursive generator." ""  n ,  f  =  0 ,  1  while  True :  yield  f  n ,  f  =  n  +  1 ,  f  *  ( n  +  1 )

Это порождает бесконечный поток факториалов по порядку; конечная его часть может быть произведена:

def  n_factorials ( k ):  n ,  f  =  0 ,  1,  а  n  <=  k :  вывести  f  n ,  f  =  n  +  1 ,  f  *  ( n  +  1 )

Затем это может быть вызвано для получения факториалов до 5! через:

для  f  в  n_factorials ( 5 ):  print ( f )

Если нас интересует только определенный факториал, можно взять только последнее значение или объединить производство и доступ в одну функцию,

def  nth_factorial ( k ):  n ,  f  =  0 ,  1, в  то время как  n  <  k :  n ,  f  =  n  +  1 ,  f  *  ( n  +  1 )  дает  f

Как можно легко увидеть здесь, это практически эквивалентно (просто путем замены returnтолько yieldтам) методике аргумента аккумулятора для хвостовой рекурсии , развернутой в явный цикл. Таким образом, можно сказать, что концепция corecursion является экспликацией варианта осуществления итерационных вычислительных процессов с помощью рекурсивных определений, где это применимо.

Последовательность Фибоначчи [ править ]

Таким же образом последовательность Фибоначчи может быть представлена ​​как:

Поскольку последовательность Фибоначчи является рекуррентным отношением порядка 2, коркурсивное отношение должно отслеживать два последовательных члена, соответствующие сдвигу вперед на один шаг и соответствующие вычислению следующего члена. Затем это может быть реализовано следующим образом (с использованием параллельного присваивания ):

def  fibonacci_sequence ():  a ,  b  =  0 ,  1  while  True :  вывести  a  a ,  b  =  b ,  a  +  b

В Haskell,

 карта  FST  (  ( \ ( , б ) -> ( Ь , + б )) ` итерация ` ( 0 , 1 ) )     

Обход дерева [ править ]

Обход дерева с использованием подхода в глубину - классический пример рекурсии. Кроме того, обход в ширину вполне естественно может быть реализован с помощью corecursion.

Без особого использования рекурсии или corecursion можно пройти по дереву, начав с корневого узла, поместив его дочерние узлы в структуру данных, а затем итеративно удаляя узел за узлом из структуры данных, помещая потомков каждого удаленного узла обратно в эту структуру данных. . [b] Если структура данных является стеком (LIFO), это дает обход в глубину, а если структура данных является очередью (FIFO), это дает обход в ширину.

Используя рекурсию, можно реализовать обход (пост-порядок) [c] в глубину, начиная с корневого узла и рекурсивно обходя каждое дочернее поддерево по очереди (поддерево, основанное на каждом дочернем узле) - второе дочернее поддерево не запускается обработка до завершения первого дочернего поддерева. Когда достигается конечный узел или исчерпаны дочерние узлы узла ветвления, посещается сам узел (например, выводится значение самого узла). В этом случае стек вызовов (рекурсивных функций) действует как стек, по которому выполняется итерация.

Используя corecursion, можно реализовать обход в ширину, начиная с корневого узла, выводя его значение, [d] затем обходя поддеревья в ширину, т. Е. Передавая весь список поддеревьев на следующий шаг (ни один поддерево, как в рекурсивном подходе) - на следующем шаге выводится значение всех их корневых узлов, затем передаются их дочерние поддеревья и т. д. [e] В этом случае функция генератора, фактически сама выходная последовательность, действует как очередь. Как и в примере факториала (выше), где вспомогательная информация индекса (на каком шаге был первый, n ) была продвинута вперед в дополнение к фактическому выходу n!, в этом случае вспомогательная информация об оставшихся поддеревьях продвигается вперед в дополнение к фактическому выводу. Символически:

Это означает, что на каждом шаге выводится список значений корневых узлов, а затем переходит к дочерним поддеревьям. Создание только значений узлов из этой последовательности просто требует отбрасывания данных вспомогательного дочернего дерева, а затем сглаживания списка списков (значения изначально группируются по уровню (глубине); сглаживание (разгруппировка) дает плоский линейный список). В Haskell,

 concatMap  FST  (  ( \ ( v ,  т )  ->  ( rootValues  v  т ,  childTrees  т ))  ` итерация `  ( [] ,  fullTree )  )

Их можно сравнить следующим образом. Рекурсивный обход обрабатывает листовой узел ( внизу ) в качестве базового случая (когда нет дочерних элементов, просто выведите значение) и анализирует дерево на поддеревья, обходя каждое по очереди, что в конечном итоге приводит только к листовым узлам - фактическому листу узлы и узлы ветвления, чьи дочерние узлы уже были обработаны (обрезаны ниже ). В отличие от этого, коркурсивный обход обрабатывает корневой узел ( вверху ) как базовый случай (для данного узла сначала выводится значение), обрабатывает дерево как синтезируемое.корневого узла и его дочерних узлов, затем создает в качестве вспомогательного вывода список поддеревьев на каждом шаге, которые затем являются входными данными для следующего шага - дочерние узлы исходного корня являются корневыми узлами на следующем этапе, как их родители уже разобрались (обрезано выше ). В рекурсивном обходе есть различие между листовыми узлами и узлами ветвления, тогда как в коркурсивном обходе нет различия, поскольку каждый узел рассматривается как корневой узел поддерева, которое он определяет.

Примечательно, что для бесконечного дерева [f] коркурсивный обход в ширину будет проходить все узлы, как и для конечного дерева, в то время как рекурсивный обход в глубину будет проходить вниз по одной ветви, а не по всем узлам, и действительно, если обход пост-порядок, как в этом примере (или по порядку), он вообще не будет посещать узлы, потому что он никогда не достигает листа. Это показывает полезность corecursion, а не рекурсии для работы с бесконечными структурами данных.

В Python это можно реализовать следующим образом. [g] Обычный обход в глубину после порядка может быть определен как: [h]

Защита  ДФ ( узел ):  «» «пост-порядок глубина первого обход». «»  если  узел  не является  не  None :  ДФ ( узел . влево )  ф.р. ( узел . правый )  печать ( узел . значение )

Затем он может быть вызван, df(t)чтобы распечатать значения узлов дерева в порядке пост-порядка по глубине.

Коркурсивный генератор в ширину можно определить как: [i]

def  bf ( tree ):  "" "Базовый генератор в ширину." ""  tree_list  =  [ tree ]  while  tree_list :  new_tree_list  =  []  для  дерева  в  tree_list :  если  tree  is  not  None :  получить  дерево . значение  new_tree_list . append ( tree . left )  new_tree_list . добавить ( дерево . справа )  tree_list =  new_tree_list

Затем его можно вызвать для печати значений узлов дерева в порядке в ширину:

для  i  в  bf ( t ):  print ( i )

Определение [ править ]

Исходные типы данных можно определить как наименьшую фиксированную точку (с точностью до изоморфизма ) некоторого уравнения типа; тогда изоморфизм задается исходной алгеброй . Соответственно, окончательные (или оконечные) типы данных могут быть определены как наибольшая фиксированная точка уравнения типа; тогда изоморфизм задается финальной коалгеброй .

Если предметом обсуждения является категория множеств и общих функций, то окончательные типы данных могут содержать бесконечные, необоснованные значения, тогда как исходные типы - нет. [1] [2] С другой стороны, если предметом обсуждения является категория полных частичных порядков и непрерывных функций , что примерно соответствует языку программирования Haskell , то конечные типы совпадают с начальными типами, а соответствующая конечная коалгебра и исходная алгебра образуют изоморфизм. [3]

Таким образом, Corecursion - это метод рекурсивного определения функций, диапазон которых (codomain) является конечным типом данных, двойственным тому, как обычная рекурсия рекурсивно определяет функции, домен которых является начальным типом данных. [4]

Ниже приводится несколько примеров на Haskell, которые различают corecursion. Грубо говоря, если перенести эти определения в категорию множеств, они все равно будут коркурсивными. Это неформальное использование согласуется с существующими учебниками по Haskell. [5] Примеры, используемые в этой статье, предшествуют попыткам дать определение corecursion и объяснить, что это такое.

Обсуждение [ править ]

Правило для примитивной рекурсии для кодированных является двойным правилу для примитивной рекурсии для данных. Вместо того, чтобы переходить к аргументу путем сопоставления с образцом в его конструкторах (которые были вызваны где-то раньше , поэтому мы получаем готовые данные и попадаем в его составные части, то есть "поля"), мы поднимаемся по результату заполнив его «деструкторы» (или «наблюдатели», которые будут где-то вызываться позже - так что мы фактически вызываем конструктор, создавая еще один бит результата, который будет наблюдаться позже). Таким образом, corecursion создает (потенциально бесконечные) коды, тогда как обычный рекурсивный анализ(обязательно конечные) данные. Обычная рекурсия может быть неприменима к кодам, потому что она может не завершаться. И наоборот, corecursion не является строго необходимым, если тип результата - данные, потому что данные должны быть конечными.

В «Программировании с потоками в Coq: пример: Решето Эратосфена» [6] мы находим

hd  ( conc  a  s )  =  a  tl  ( conc  a  s )  =  s( sieve  p  s )  =  if  div  p  ( hd  s ),  затем  sieve  p  ( tl  s )  else  conc  ( hd  s )  ( sieve  p  ( tl  s ))hd  ( простые числа  s )  =  ( hd  s )  tl  ( простые числа  s )  =  простые числа  ( решето  ( hd  s )  ( tl  s ))

где простые числа "получены применением операции простых чисел к потоку (Enu 2)". Следуя приведенным выше обозначениям, последовательность простых чисел (с префиксом 0 к нему) и чисел, последовательно просеиваемых потоками, может быть представлена ​​как

или в Haskell,

( \ ( Р ,  S @ ( ч : т ))  ->  ( ч ,  решето  ч  т ))  ` итерация `  ( 0 ,  [ 2 .. ])

Авторы обсуждают, что определение sieveне всегда будет продуктивным и может застрять, например, при вызове [5,10..]в качестве начального потока.

Вот еще один пример на Haskell. Следующее определение дает список чисел Фибоначчи за линейное время:

ФИБС  =  0  :  1  :  zipWith  ( + )  ФИБС  ( хвост  ФИБС )

Этот бесконечный список зависит от ленивого вычисления; элементы вычисляются по мере необходимости, и только конечные префиксы когда-либо явно представлены в памяти. Эта функция позволяет завершать работу алгоритмов в части кодовых данных; такие методы являются важной частью программирования на Haskell.

Это также можно сделать в Python: [7]

из  itertools  import  tee ,  chain ,  islice ,  imapdef  add ( x ,  y ):  вернуть  x  +  ydef  fibonacci ():  def  deferred_output ():  for  i  in  output :  yield  i  result ,  c1 ,  c2  =  tee ( deferred_output (),  3 )  paired  =  imap ( add ,  c1 ,  islice ( c2 ,  1 ,  None ))  output  =  цепочка ([ 0 ,  1 ],  парный )  возвращает  результатдля  i  в  islice ( fibonacci (),  20 ):  print ( i )

Определение zipWithможет быть встроено, что приводит к следующему:

fibs  =  0  :  1  :  следующий  fibs  где  next  ( a :  t @ ( b : _ ))  =  ( a + b ) : следующий  t

В этом примере используется самореферентная структура данных . Обычная рекурсия использует самореференционные функции , но не вмещает самореференциальные данные. Однако для примера Фибоначчи это несущественно. Его можно переписать следующим образом:

fibs  =  fibgen  ( 0 , 1 ) fibgen  ( x , y )  =  x  :  fibgen  ( y , x + y )

Это использует только самореференционную функцию для построения результата. Если бы он использовался со строгим конструктором списка, это был бы пример неконтролируемой рекурсии, но с нестрогим конструктором списка эта защищенная рекурсия постепенно создает неопределенно определенный список.

Corecursion не обязательно создает бесконечный объект; Коркурсивная очередь [8] - особенно хороший пример этого явления. Следующее определение производит обход двоичного дерева в ширину за линейное время:

 дерево  данных a  b  =  лист  a  |  Ветка  b  ( Дерево  a  b )  ( Дерево  a  b )bftrav  ::  Tree  a  b  ->  [ Tree  a  b ] bftrav  tree  =  queue,  где  queue  =  tree  :  gen  1  queue gen  0  p  =  []  gen  len  ( Leaf  _  :  s )  =  gen  ( len - 1 )  s  gen  len  ( Branch  _  l  r  :  s )  =  l  :  r  :  gen  ( len + 1 )  s

Это определение берет исходное дерево и создает список поддеревьев. Этот список служит двойной цели: как очередь, так и результат ( gen len pвыводит lenвыемки после обратного указателя ввода p, вдоль queue). Оно конечно тогда и только тогда, когда исходное дерево конечно. Длина очереди должна явно отслеживаться, чтобы гарантировать завершение; это можно безопасно исключить, если это определение применяется только к бесконечным деревьям.

Другой особенно хороший пример дает решение проблемы маркировки в ширину. [9] Функция labelпосещает каждый узел в двоичном дереве по принципу «сначала в ширину» и заменяет каждую метку целым числом, каждое последующее целое число больше последнего на единицу. Это решение использует самореференциальную структуру данных, а двоичное дерево может быть конечным или бесконечным.

label  ::  Tree  a  b  ->  Tree  Int  Int  label  t  =  t ′,  где  ( t ,  ns )  =  go  t  ( 1 : ns ) go  ::  Tree  a  b  ->  [ Int ]  ->  ( Tree  Int  Int ,  [ Int ])  go  ( Leaf  _  )  ( n : ns )  =  ( Leaf  n  ,  n + 1  :  ns  )  go  ( Branch  _  l  r )  ( n : ns )  =  ( Ветвь  n  l  r ,  N + 1  :  ns ′ ′ ),  где  ( l ,  ns  )  =  go  l  ns  ( r ,  ns ′ ′ )  =  go  r  ns 

Apomorphism (например, анаморфизм , такие как разворачиваться ) является формой корекурсии таким же образом , что paramorphism (например, катаморфизм , такими как складка ) является одной из форм рекурсии.

Coq доказательство помощник поддерживает корекурсия и коиндукции с помощью команды CoFixpoint.

История [ править ]

Corecursion, называемый циклическим программированием, датируется, по крайней мере, ( Bird 1984 ), который упоминает Джона Хьюза и Филипа Уодлера ; более общие формы были разработаны в ( Allison 1989 ) . Первоначальная мотивация заключалась в создании более эффективных алгоритмов (позволяющих в некоторых случаях передавать данные вместо нескольких проходов) и реализации классических структур данных, таких как двусвязные списки и очереди, на функциональных языках.

См. Также [ править ]

  • Бисимуляция
  • Коиндукция
  • Рекурсия
  • Анаморфизм

Заметки [ править ]

  1. ^ Не проверять входные данные.
  2. ^ Более элегантно, можно начать с помещения самого корневого узла в структуру данных, а затем запустить процесс.
  3. ^ Пост-заказ состоит в том, чтобы сделать "листовой узел - базовый случай" явным для описания, но тот же анализ работает для предварительного заказа или для упорядоченного.
  4. ^ Обход в ширину, в отличие от поиска в глубину, является однозначным и обращается к значению узла перед обработкой дочерних элементов.
  5. ^ Технически можно определить обход в ширину на упорядоченном, несвязном наборе деревьев - сначала корневой узел каждого дерева, затем потомки каждого дерева по очереди, затем внуки по очереди и т. Д.
  6. ^ Предположим фиксированный коэффициент ветвления (например, двоичный) или, по крайней мере, ограниченный и сбалансированный (бесконечный во всех направлениях).
  7. ^ Сначала определяем древовидный класс, скажем, через:
     дерево классов :  def  __init__ ( self ,  value ,  left = None ,  right = None ):  self . Значение  =  значение  собственной . left  =  левый  я . right  =  право Защиту  __str__ ( само ):  возвращение  ул ( само . значение )

    и инициализировать дерево, скажем, через:

    t  =  Дерево ( 1 ,  Дерево ( 2 ,  Дерево ( 4 ),  Дерево ( 5 )),  Дерево ( 3 ,  Дерево ( 6 ),  Дерево ( 7 )))

    В этом примере узлы помечены в порядке убывания ширины:

     1 2 34 5 6 7
  8. ^ Интуитивно функция выполняет итерацию по поддеревьям (возможно, пустым), а затем после их завершения остается только сам узел, значение которого затем возвращается; это соответствует обработке листового узла как основного.
  9. ^ Здесь аргумент (и переменная цикла) рассматривается как целое, возможное бесконечное дерево, представленное (идентифицированное) его корневым узлом (дерево = корневой узел), а не как потенциальный листовой узел, отсюда и выбор имени переменной.

Ссылки [ править ]

  1. ^ Барвайз и Мосс 1996.
  2. ^ Мосс и Даннер 1997.
  3. Перейти ↑ Smyth and Plotkin 1982.
  4. ^ Гиббонс и Хаттон 2005.
  5. ^ Doets и ван Eijck 2004.
  6. ^ Leclerc и Паулин-Möhring, 1994
  7. ^ Hettinger 2009.
  8. Allison 1989; Смит 2009.
  9. ^ Джонс и Гиббонс 1992.
  • Птица, Ричард Симпсон (1984). «Использование циклических программ для исключения многократного обхода данных». Acta Informatica . 21 (3): 239–250. DOI : 10.1007 / BF00264249 .
  • Ллойд Эллисон (апрель 1989 г.). «Циркулярные программы и самореферентные структуры» . Практика и опыт работы с программным обеспечением . 19 (2): 99–109. DOI : 10.1002 / spe.4380190202 .
  • Герайнт Джонс и Джереми Гиббонс (1992). Алгоритмы линейного времени в ширину: упражнение по арифметике складок и застежек (Технический отчет). Кафедра компьютерных наук Оклендского университета.
  • Джон Барвайз ; Лоуренс С. Мосс (июнь 1996 г.). Порочные круги . Центр изучения языка и информации. ISBN 978-1-57586-009-1. Архивировано из оригинала на 2010-06-21 . Проверено 24 января 2011 .
  • Лоуренс С. Мосс; Норман Даннер (1997). «Об основах курса». Логический журнал IGPL . 5 (2): 231–257. CiteSeerX  10.1.1.40.4243 . DOI : 10.1093 / jigpal / 5.2.231 .
  • Кис Доетс; Ян ван Эйк (май 2004 г.). Путь Haskell к логике, математике и программированию . Публикации Королевского колледжа. ISBN 978-0-9543006-9-2.
  • Дэвид Тернер (2004-07-28). «Полное функциональное программирование» . Журнал универсальных компьютерных наук . 10 (7): 751–768. DOI : 10.3217 / jucs-010-07-0751 .
  • Джереми Гиббонс; Грэм Хаттон (апрель 2005 г.). «Методы доказательства для курсовых программ» . Fundamenta Informaticae . 66 (4): 353–366.
  • Леон П. Смит (2009-07-29), "Corecursive Queues Ллойда Эллисона: почему продолжения имеют значение" , The Monad Reader (14): 37–68
  • Раймонд Хеттингер (19 ноября 2009 г.). «Рецепт 576961: Методика циклической итерации» .
  • М.Б. Смит и Г.Д. Плоткин (1982). "Теоретико-категориальное решение рекурсивных уравнений области" (PDF) . SIAM Journal on Computing . 11 (4): 761–783. DOI : 10.1137 / 0211062 .
  • Леклерк, Франсуа; Полин-Моринг, Кристина (1993). Программирование с помощью потоков в Coq: пример: решето Эратосфена . Типы доказательств и программ: международный семинар TYPES '93. Springer-Verlag New York, Inc., стр. 191–212. ISBN 978-3-540-58085-0.