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 ...