1

Is it possible to define using the Isabelle proof assistant a theory involving functions of variable arity ?

For example, I would like to define the theory of all predicates of arity n, which are invariant by cyclic permutation. Given a type T and an integer n, I would like to define the theory of all predicates of arity n which verify for example: P A_1,... A_n <-> P A_n A_2, ..., A_n-1.

In Coq it is possible using dependent types, I am wondering if there is a way to express this using Isabelle ?

2 Answers 2

1

Isabelle/HOL supports functions with arbitrary, but fixed arity to some extent. The standard trick is to encode the arity of the function in its type as the cardinality of a type. Thus, you effectively have just one argument which contains a fixed number of values. Of course, all variable-arity arguments of the function must be taken from the same type. In your example, the cyclicity requirement enforces this already.

For example, you can define the type of invariant predicates of arity n as follows.

  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

Here, we model a variable-arity predicate as a predicate on functions from an index set 'n to an element type 'a. The sort constraint on 'n ensures that the type defines the operations + and 1, which we use to specify the shifting. We could assume that + wraps around when an overflow occurs, but this can also be done later with type class constraints in the lemmas.

The theory Numeral_Type (in the distribution in ~~/src/HOL/Library) defines types of finite cardinality which are written as literal numbers. Addition on them does wrap around in case of an overflow. Thus, one can write

typ "(5, int) inv_pred"

to denote the type of predicates with 5 arguments over integers which are invariant under cyclic permutations. Similarly, the type (100, nat) inv_pred contains all such predicates of arity 100.

If you use plain functions to encode the variable arity arguments, there is no nice syntax to apply a function to a given list of arguments. The theory ~~/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product defines a type ('n, 'a) vec of vectors, which could be used here as well. Still, you have to define your own syntax for this, say apply_ip P [: x1, x2, x3, x4 :] and write appropriate parsers and pretty-printers.

However, Isabelle cannot do computations on the type level during type checking. Thus, you will have a hard time to type terms like

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

because 2 + 2 is not the same type as 4 in Isabelle/HOL.

1

A similar way to do n-ary functions is this: First, we define types for positive natural numbers:

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

Now we define the type of n ary functions that take n values of type 'a and return a 'b as the type of functions that take a functon from 'n ⇒ 'a and return a 'b, and absraction and application for these functions:

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)

Add some syntatical sugar:

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"

Now you can write the type of 'n-ary functions that take 'n values of type 'a and return a 'b as 'a ^ 'n ⇒ 'b, and you can use χ like Lambda abstraction and $ like function application:

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" *)

Whether my formulation of Andreas's is more convenient for you depends on what exactly you want to do with your functions, I suppose.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.