Литейный листок и сжатие Isabelle

Question

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

Код:

theory Scratch 
imports Main Nat 
begin 
    value "let a = {(1::int), 2, 3, 4} in (let b = {(6::int),7,8,9} in 
    ((1::int), 6) ∈ set (filter (λ el . (snd el) < 8) [(n,m). n ∈ a ∧ m ∈ b]))" 
end 

В результате я ожидал был истинным или ложным. Результаты были:

"(1, 6) 
∈ set [u←if (1 = n ∨ 2 = n ∨ 3 = n ∨ 4 = n) ∧ 
      (6 = m ∨ 7 = m ∨ 8 = m ∨ 9 = m) 
      then [(n, m)] else [] . snd u < 8]" 
    :: "bool" 

1. Почему результат не вычисляться в True/False значения?
2. Можно ли написать код, где функции фильтра оцениваются по набору, а не списку?

Answer 1

Прежде всего, вы не можете конвертировать множества в списки. Списки имеют определенный порядок элементов; наборов нет.

Вопрос 1

Это потому, что у вас есть свободные переменные в них: n и m. Выражение [(n,m). n ∈ a ∧ m ∈ b] в основном означает if n ∈ a ∧ m ∈ b then [(n,m)] else []. Это не то, что вы хотите.

Если a и b были списком, вы можете использовать синтаксис понимания списка [(n,m). n ← a, m ← b]. Однако, поскольку и b являются наборами, это не может работать, так как результатом будет список с определенным порядком, и этот порядок должен быть от где-то - но a и b, как наборы, не имеют такого заказа.

Вопрос 2

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

В Isabelle есть раздел, посвященный изысканности code generation manual. Я рекомендую вам взглянуть на него.

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

Однако следующий потерпит неудачу из-за ошибки wellsortedness:

value "let a = {(1::int), 2, 3, 4} in (let b = {(6::int),7,8,9} in 
    ((1::int), (6 :: int)) ∈ Set.filter (λ el . (snd el) < 8) {x. fst x ∈ a ∧ snd x ∈ b})" 

Это потому, что набор постижения (т.е. {x. … }) являются, в общем, не вычислит. Вы должны заменить это {x. fst x ∈ a ∧ snd x ∈ b} тем, что генератор кода может генерировать код. В этом случае это легко, потому что эта операция является всего лишь декартовым продуктом.Вы можете написать:

value "let a = {(1::int), 2, 3, 4} in (let b = {(6::int),7,8,9} in 
    ((1::int), (6 :: int)) ∈ Set.filter (λ el . (snd el) < 8) (a × b))" 

И вы получите ожидаемый результат.