(* Translating De Bruijn notation to nominal notation. This code snippet is particularly easy in terms of proof obligations. *) (* De Bruijn indices, expressed in unary notation, since we have no primitive integers yet. *) type dbindex = | IZero | ISucc of dbindex (* De Bruijn style lambda-terms. *) type dbterm = | DBVar of dbindex | DBLambda of dbterm | DBApp of dbterm * dbterm (* Nominal style lambda-terms. *) type term = | Var of atom | Lambda of < atom * inner term > | App of term * term (* Environments for translating De Bruijn terms to nominal terms. *) type env = | ENil | ECons of env * atom (* The translation code. *) fun find accepts env, index produces a = case env, index of | ECons (_, x), IZero -> x | ECons (env, _), ISucc (index) -> find (env, index) end fun import accepts env, dbterm produces term = case dbterm of | DBVar (index) -> Var (find (env, index)) | DBLambda (dbterm) -> fresh x in Lambda (x, import (ECons (env, x), dbterm)) | DBApp (dbterm1, dbterm2) -> App (import (env, dbterm1), import (env, dbterm2)) end fun main accepts dbterm produces term where free(term) == empty (* postcondition not required, but we can prove that it holds *) = import (ENil, dbterm) (* The reverse translation. *) fun lookup accepts env, a where free(a) <= free(env) produces index = case env of | ENil -> absurd | ECons (env, b) -> if a == b then IZero else ISucc (lookup (env, a)) end end fun export accepts env, t where free(t) <= free(env) produces dbterm = case t of | Var (x) -> DBVar (lookup (env, x)) | Lambda (x, t) -> DBLambda (export (ECons (env, x), t)) | App (t1, t2) -> DBApp (export (env, t1), export (env, t2)) end fun malabar accepts t where free(t) == empty produces dbterm = export (ENil, t)