Функция переменной функции в Isabelle

Question

Можно ли определить с помощью помощника по проверке Isabelle теорию, включающую функции переменной arity?

Например, я хотел бы определить теорию всех предикатов arity n, инвариантных циклической перестановкой. Учитывая тип T и целое число n, Я хотел бы определить теорию всех предикатов arity n, которые проверяют, например: P A_1, ... A_n < -> P A_n A_2, ..., A_n-1 ,

В Coq можно использовать зависимые типы, мне интересно, есть ли способ выразить это с помощью Isabelle?

Answer 1

Isabelle/HOL поддерживает функции с произвольной, но фиксированной аркой в ​​некоторой степени. Стандартный трюк состоит в том, чтобы кодировать арность функции в своем типе как мощность типа. Таким образом, у вас фактически есть только один аргумент, который содержит фиксированное количество значений. Конечно, все аргументы переменной-аргумента функции должны быть взяты из одного и того же типа. В вашем примере требование цикличности уже применяет это.

Например, вы можете определить тип инвариантных предикатов arity n следующим образом.

typedef ('n :: "{one, plus}", 'a) inv_pred 
    = "{P :: ('n ⇒ 'a) ⇒ bool. ∀f. P f ⟷ P (λn. f (n + 1))}" 
    morphisms apply_ip Abs_inv_pred 
    by blast 

Здесь мы моделируем с переменной Arity предикат как предикат на функции из индекса устанавливается 'n к типу 'a элемента. Ограничение сортировки на 'n гарантирует, что тип определяет операции + и 1, которые мы используем для указания сдвига. Мы могли бы предположить, что + обертывается, когда происходит переполнение, но это также можно сделать позже с ограничениями класса классов в леммах.

Теория Numeral_Type (в распределении в ~~/src/HOL/Library) определяет типы конечной мощности, которые записываются как буквальные числа. Добавление на них обертывается в случае переполнения. Таким образом, можно написать

typ "(5, int) inv_pred" 

для обозначения типа сказуемых с 5 аргументов над целыми числами, которые инвариантны относительно циклических перестановок. Аналогично, тип (100, nat) inv_pred содержит все такие предикаты arty 100.

Если вы используете простые функции для кодирования аргументов переменной arity, нет сильного синтаксиса для применения функции к данному списку аргументов. Теория ~~/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product определяет тип векторов ('n, 'a) vec, которые также могут быть использованы здесь. Тем не менее, вы должны определить свой собственный синтаксис для этого, скажем apply_ip P [: x1, x2, x3, x4 :] и написать соответствующие синтаксические анализаторы и симпатичные принтеры.

Однако Изабель не может выполнять вычисления на уровне типа во время проверки типа. Таким образом, вы будете иметь трудное время, чтобы ввести такие термины, как

apply_ip P ([: x1, x2 :] ++ [: x3, x4 :]) 

потому 2 + 2 не тот же тип 4 в Isabelle/HOL.

Answer 2

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

theory foo 
imports Main "~~/src/HOL/Library/Cardinality" "~~/src/Tools/Adhoc_Overloading" 
begin 

typedef num1 = "UNIV :: unit set" 
    by (rule UNIV_witness) 

typedef 'n suc = "UNIV :: ('n::finite) option set" 
    by (rule UNIV_witness) 

instance num1 :: finite 
proof 
    show "finite (UNIV :: num1 set)" 
    unfolding type_definition.univ[OF type_definition_num1] 
    using finite by (rule finite_imageI) 
qed 

instance suc :: (finite) finite 
proof 
    show "finite (UNIV :: ('n::finite) suc set)" 
    unfolding type_definition.univ[OF type_definition_suc] 
    using finite by (rule finite_imageI) 
qed 

setup_lifting type_definition_num1 

Теперь определим тип n ичных функций, которые принимают n значения типа 'a и возвращать 'b как тип функций, которые принимают functon от 'n ⇒ 'a и возвращают 'b и absraction и применение для этих функций:

typedef ('a,'n,'b) nary_fun = "UNIV :: (('n::finite ⇒ 'a) ⇒ 'b) set" 
    by (rule UNIV_witness) 

setup_lifting type_definition_suc 
setup_lifting type_definition_nary_fun 

lift_definition nary_fun_apply_1 :: "('a,num1,'b) nary_fun ⇒ 'a ⇒ 'b" 
    is "λf x. f (λ_. x)" . 

lift_definition nary_fun_apply_suc :: "('a,('n::finite) suc,'b) nary_fun ⇒ 'a ⇒ ('a,'n,'b) nary_fun" 
    is "λ(f::('n option ⇒ 'a) ⇒ 'b) (x::'a) (y::'n ⇒ 'a). f (case_option x y)" . 

lift_definition nary_fun_abs_1 :: "('a ⇒ 'b) ⇒ ('a,num1,'b) nary_fun" 
    is "λf x. f (x())" . 

lift_definition nary_fun_abs_suc :: "('a ⇒ ('a,'n::finite,'b) nary_fun) ⇒ ('a,'n suc,'b) nary_fun" 
    is "λf x. f (x None) (λn. x (Some n))" . 

lemma nary_fun_1_beta [simp]: "nary_fun_apply_1 (nary_fun_abs_1 f) x = f x" 
    by (simp add: nary_fun_abs_1_def nary_fun_apply_1_def Abs_nary_fun_inverse) 

lemma nary_fun_suc_beta [simp]: "nary_fun_apply_suc (nary_fun_abs_suc f) x = f x" 
    by (simp add: nary_fun_abs_suc_def nary_fun_apply_suc_def Abs_nary_fun_inverse 
       Abs_suc_inverse Rep_nary_fun_inverse) 

Добавьте syntatical сахар:

consts nary_fun_apply :: "('a,('n::finite),'b) nary_fun ⇒ 'a ⇒ 'c" (infixl "$" 90) 

adhoc_overloading nary_fun_apply nary_fun_apply_1 nary_fun_apply_suc 

syntax 
    "_nary_fun_abs" :: "pttrns ⇒ 'b ⇒ ('a,'n,'b) nary_fun" ("χ (_). _" 10) 

translations 
    "χ x y. e" == "CONST nary_fun_abs_suc (λx. (χ y. e))" 
    "χ x. e" == "CONST nary_fun_abs_1 (λx. e)" 

syntax 
    "_NumeralType" :: "num_token => type" ("_") 
    "_NumeralType1" :: type ("1") 

translations 
    (type) "1" == (type) "num1" 

parse_translation {* 
    let 
    fun mk_numtype n = 
     if n = 1 then Syntax.const @{type_syntax num1} 
     else if n < 0 then raise TERM ("negative type numeral", []) 
     else Syntax.const @{type_syntax suc} $ mk_numtype (n - 1) 

    fun numeral_tr [Free (str, _)] = mk_numtype (the (Int.fromString str)) 
     | numeral_tr ts = raise TERM ("numeral_tr", ts); 

    in [(@{syntax_const "_NumeralType"}, K numeral_tr)] end; 
*} 

print_translation {* 
    let 
    fun int_of (Const (@{type_syntax num1}, _)) = 1 
     | int_of (Const (@{type_syntax suc}, _) $ t) = 1 + int_of t 
     | int_of t = raise TERM ("int_of", [t]); 

    fun suc_tr' [t] = 
      let 
      val num = string_of_int (int_of t + 1) handle TERM _ => raise Match; 
      in 
      Syntax.const @{syntax_const "_NumeralType"} $ Syntax.free num 
      end 
     | suc_tr' _ = raise Match; 
    in 
    [(@{type_syntax suc}, K suc_tr')] 
    end; 
*} 

syntax 
    "_nary_fun_type" :: "type ⇒ type ⇒ type ⇒ type" ("(_ ^/ _ ⇒/ _)" [15, 16, 15] 15) 

translations 
    (type) "'a^'n ⇒ 'b" == (type) "('a,'n,'b) nary_fun" 

Теперь вы можете написать тип 'n -ичных функций, которые принимают 'n значения типа 'a и возвращают 'b в 'a^'n ⇒ 'b, и вы можете использовать χ как лямбда-абстракции и $ как применение функции:

lemma "(χ x y. (x, y)) $ 1 $ 2 = (1,2)" by simp 

term "(χ x y z. (x, y + z))" 
(* "χ x y z. (x, y + z)" :: "'a^3 ⇒ 'a × 'a" *) 

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