Проблемы с завершением рекурсивной функции с использованием zip, map и products - PullRequest
Новая
       23

Проблемы с завершением рекурсивной функции с использованием zip, map и products

0 голосов
/ 26 июня 2018

Я столкнулся с проблемой при попытке определить рекурсивную функцию, которая использует карту поверх zip.

Вот упрощенная версия моего кода, во-первых, которая работает 

datatype bar = Bar "bar list"

function (sequential) bar_lub :: "[bar,bar] ⇒ bar" ("_⊔b_" [30,60] 60)
  where
    "(Bar ts) ⊔b (Bar us) = Bar (map (λ(t1,t2). t1 ⊔b t2) (zip ts us))"
  by pat_completeness auto

Это нормально и приводит к цели прекращения действия 

1. ⋀ts us a b. (a, b) ∈ set (zip ts us) ⟹ P (a, b) ~ P (Bar ts, Bar us)

, что легко доказать при наличии соответствующих P и ~.

Моя проблема возникает, когда я изменяю список на список пар следующим образом

тип данных 'a foo = Foo "(' a foo × 'a) list" 

function (sequential) foo_lub1 :: "['a foo, 'a foo] ⇒ 'a foo" ("_⊔_" [30,60] 60)
  where
    "(Foo ts) ⊔ (Foo us) = Foo (map (λ((t1,_), (t2,_)). (t1 ⊔ t2, undefined)) (zip ts us))"
  by pat_completeness auto

Теперь мы получаем цель завершения 

1. ⋀ts us t1 b1 t2 b2 xc. ((t1, b1), t2, b2) ∈ set (zip ts us) ⟹ P (t1, xc) ~ P (Foo ts, Foo us)

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

Кто-нибудь знает, почему это происходит, и есть ли способы исправить это?

1 Ответ

0 голосов
/ 26 июня 2018

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

function (sequential) foo_lub1 :: "['a foo, 'a foo] ⇒ 'a foo" ("_⊔_" [30,60] 60)
  where
    "(Foo ts) ⊔ (Foo us) = Foo (map (λx. (fst (fst x) ⊔ fst (snd x), undefined)) (zip ts us))"
...