LRI
Équipe MODHEL
Bât 650 Ada Lovelace, Université Paris Sud
Rue Noetzlin, 91190 Gif-sur-Yvette, France
Isabelle club meeting on December 16 2015

Audience

  • Thibaut Balabonski
  • Safouan Taha
  • Yakoub Nemouchi
  • Frédéric Tuong
  • Burkhart Wolff
  • Jean-Marie Madiot
  • Lina Ye

Pearl

Benoit

Nominals in Isabelle

Motivation

  • representations des calculs lambda, PCF ou variants avec points fixes, matching.
  • modèles de machine rereduction avec d’état

Facon standard : calcul de Bruin

  • dantesque
  • explicit deBruin lift counterintuitive and difficult to handle
  • error prone, often not feasible.
  • complications in proofs

Solution: Theory of nominal types providing a built-in notion of bound variables.

Theorie

  • TYP X : “the terms”
           ([(x,y)] $ λx. x) = λy. y     
  • TYP A : atomes “the variables"
    • enumerable
    • infini
    Perm A = ensembles de permutations sur A a support fini
  • OP * : Perm A × X ⇒ X " the renaming"
  • OP $ : Perm A × A ⇒ A " lookup"
    • Properties:
    π_1 $ (π_2 $ x) = (π_1 o π_2) $ x
    id $ x = x
  • Interpretation of nominal type: (X, *)
     such that all (x ∈ X) are a finite support called supp(x) 
  • ∀ π ∈ Perm A,
  • ∀ ∈ supp(x). π a = a) π $ x = x

Implementation in Isabelle/Nominal:

atom_decl name

nominal_datatype lam = Var name
                     | App lam lam
                     | Lam <<name>>. lam

This presentation in Isar syntax is internally mapped to a raw datatype.

In HOL :

datatype φ = PVar name
           | Papp (φ x φ)
           | PLam “name ⇒ (φ option)”

The subset π_α is defined inductively:

  • PVar(a) ∈ φ_α
  • t_1, t_2 ∈ φ_α ⟹ Papp (t_1, t_2) ∈ φ_α
  • a ∈ A, t ∈ φ_α ⟹ PLam [a]$t ∈ φ_α
       where

       [a]$t = λ b. (if a = b then Some t 
                              else if b # t then Some(a,b) $ t 
                                   else None)

Demo by Benoit.

Applications

  • diverse lambda calculi,
  • CCS --- with dynamic creation of channels that works ...


Previous meeting -- Next meeting