Не могу определить прекращение

Функция для определения, является ли набор подмножеством другого:

Fixpoint subset (s1:bag) (s2:bag) : bool :=
  match s1 with
  | nil => true
  | h :: t => match (beq_nat (count h s1) (count h s2)) with
    | true => subset (remove_all h t) (remove_all h s2)
    | false => false
    end
  end.

Для ясности

  • beq_nat определяет равенство двух натуральных чисел
  • count подсчитывает, сколько раз данное натуральное число встречается в наборе
  • remove_all удаляет каждый экземпляр данного натурального числа из набора

CoqIDE «Не удается угадать убывающий аргумент исправления». Учитывая, что рекурсия выполняется на подмножестве t (хвост s1), почему это не гарантирует завершение?

Примечание. Эта проблема возникла на этом веб-сайте, авторы которого просят не размещены публично. Более того, я уже решил это упражнение, так что решение нежелательно. Объяснение того, почему coq не может определить завершение, было бы весьма признательно.


termination coq totality
person Alex    schedule 16.01.2018    source источник

Ответы (2)


arrow_upward
5
arrow_downward

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

Вот пример:

Fixpoint plus (n m : nat) : nat :=
  match n with
  | O => m
  | S p => S (plus p m)
  end.

Объяснение принятия состоит в том, что p является аргументом с рангом 1, он получается как переменная сопоставления с образцом из n, который является начальным аргументом с рангом 1. Таким образом, функция является структурно рекурсивной, убывающей по первому аргументу. Всегда должен быть аргумент, который уменьшает. Комбинированное уменьшение между несколькими аргументами не допускается.

Вам следует прекратить читать здесь, если вы не хотите утонуть в деталях.

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

Require Import List Arith.

Fixpoint awk1 (l : list nat) :=
  match l with
  | a :: ((b :: l'') as l') => 
    b :: awk1 (if Nat.even a then l' else l'')
  | _ => l
  end.

Итак, в функции awk1 рекурсивный вызов не переменной, а выражения сопоставления с шаблоном, но это нормально, поскольку все возможные значения этого рекурсивного вызова действительно являются переменными, полученными путем сопоставления с шаблоном. Это также показывает, насколько привередливым может быть средство проверки завершения, потому что выражение (if Nat.even a then (b :: l'') else l'') не будет принято: (b :: l'') не является переменной.

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

Definition arg n (l : list nat) :=
  if Nat.even n then
    l 
  else
    match l with _ :: l' => l' | _ => l end.

Fixpoint awk2 (l : list nat) :=
match l with
  a :: l' => a :: awk2 (arg a l')
| _ => l
end.

Третье ослабление правила заключается в том, что функция, используемая для вычисления рекурсивного аргумента, может даже быть рекурсивной, если она может рекурсивно передавать свойство убывания. Вот иллюстрация:

Fixpoint mydiv (n : nat) (m : nat) :=
   match n, m with
     S n', S m' => S (mydiv (Nat.sub n' m') m)
   | _, _ => n
   end.

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

person Yves    schedule 17.01.2018

arrow_upward
2
arrow_downward

Ваш аргумент о прекращении верен, но Coq недостаточно умен, чтобы понять это самостоятельно. Грубо говоря, Coq принимает только рекурсивные вызовы, выполняемые над синтаксическими подтермами своего главного аргумента. Это очень ограничительное понятие: например, [1; 3] — это подсписок [0; 1; 2; 3], но не синтаксический подтермин.

Если вы хотите, чтобы Coq принял это, вам, вероятно, придется переписать свою функцию, используя хорошо обоснованную рекурсию. В книге Адама Чипалы CPDT есть хорошая глава на эту тему.

person Arthur Azevedo De Amorim    schedule 16.01.2018