Nondeterminism and Meta

Stream: new members

[Logan Murphy]

Hi all,
I'm working on translating as much as I can of Winskel's Formal Semantics of Programming Languages into Lean, and of course there is trouble with representing while loops as recursive functions. I know that the Hitchhiker's guide uses inductive predicates to get around this, but I'm wondering if their are any other workarounds? I can get Lean to type-check my function with the meta keyword, but I haven't been able to find documentation references for what this does. What am I losing by using meta?

namespace imperative

def Loc : Type := string
variables X Y : Loc

inductive Aexp : Type
| num : ℤ → Aexp
| loc : Loc → Aexp
| add : Aexp → Aexp → Aexp
| sub : Aexp → Aexp → Aexp
| mul : Aexp → Aexp → Aexp

def state : Type := Loc → ℤ

@[instance] def Aexp.has_zero : has_zero Aexp := ⟨Aexp.num 0⟩
@[instance] def Aexp.has_one : has_one Aexp := ⟨Aexp.num 1⟩
@[instance] def Aexp.has_add : has_add Aexp := ⟨Aexp.add⟩
@[instance] def Aexp.has_sub : has_sub Aexp := ⟨Aexp.sub⟩
@[instance] def Aexp.has_mul : has_mul Aexp := ⟨Aexp.mul⟩

def aexp_eval (σ : state) : Aexp → ℤ
| (Aexp.num n) := n
| (Aexp.loc l) := σ l
| (Aexp.add m n) := aexp_eval m + aexp_eval n
| (Aexp.sub m n) := aexp_eval m - aexp_eval n
| (Aexp.mul m n) := aexp_eval m * aexp_eval n

notation ⟨a, σ⟩ := aexp_eval σ a

def aexp_reduce : state → Aexp → ℤ → Prop := λ σ a n, ⟨a, σ⟩ = n
notation ⟨a, σ⟩ ` ↠ ` n := aexp_reduce σ a n

def aexp_equiv : Aexp → Aexp → Prop := λ a₁ a₂,
∀ (n : ℤ) (σ : state), (⟨a₁, σ⟩ ↠ n) ↔ (⟨a₂, σ⟩ ↠ n)

notation a₁ ` ∼ ` a₂ := aexp_equiv a₁ a₂

inductive Bexp : Type
| T : Bexp
| F : Bexp
| eq : Aexp → Aexp → Bexp
| lte : Aexp → Aexp → Bexp
| neg : Bexp → Bexp
| conj : Bexp → Bexp → Bexp
| disj : Bexp → Bexp → Bexp

def bexp_eval (σ : state) : Bexp → bool
| Bexp.T := tt
| Bexp.F := ff
| (Bexp.eq a₁ a₂) := if (⟨a₁,σ⟩ = ⟨a₂, σ⟩) then tt else ff
| (Bexp.lte a₁ a₂) := if (⟨a₁,σ⟩ ≤ ⟨a₂,σ⟩) then tt else ff
| (Bexp.neg b) := if (bexp_eval b) = tt then ff else tt
| (Bexp.conj b₁ b₂) := band (bexp_eval b₁) (bexp_eval b₂)
| (Bexp.disj b₁ b₂) := bor (bexp_eval b₁) (bexp_eval b₂)
notation ⟨b, σ⟩ := bexp_eval σ b

inductive Com : Type
| skip : Com
| assign : Loc → Aexp → Com
| seq : Com → Com → Com
| cond : Bexp → Com → Com → Com
| while : Bexp → Com → Com
notation c₁ `;;` c₂ := Com.seq c₁ c₂

def asgn (σ : state) (m : ℤ) (X : Loc) : state :=
λ Y, if (X = Y) then m else (σ Y)
notation σ`[`X `<-` m`]` := asgn σ m X

meta def execute : Com → state → state
| Com.skip := λ σ, σ
| (Com.assign X a) := λ σ, σ[X ← ⟨a,σ⟩]
| (c₁ ;; c₂) :=  λ σ, let σ' := (execute c₁ σ) in
                                 execute c₂ σ'
| (Com.cond b c₁ c₂) := λ σ, match ⟨b,σ⟩ with
                        |tt := execute c₁ σ
                        |ff := execute c₂ σ
                        end
| (Com.while b c) := λ σ, match ⟨b,σ⟩ with
                     | ff := σ
                     | tt := let (σ' : state) := (execute c σ) in
                              execute (Com.while b c) σ'
                     end

notation ⟨c, σ⟩ := execute c σ

meta def com_reduce : Com → state → state → Prop :=
λ c σ₁ σ₂, (execute c σ₁) = σ₂

end imperative

[Kenny Lau]

meta means "don't check if the recursion terminates"

[Kyle Miller]

Everything that is meta is outside the theory and is untrusted. Non-meta definitions and lemmas cannot refer to ones that are meta. Types of meta definitions can't be interpreted as being theorems:

meta def ohno {p : Prop} : p → false
| x := ohno x

I'm not sure whether or not meta lemmas are sound -- I at least couldn't give this last definition as a meta lemma rather than a meta def.

I think meta is supposed to refer to metaprogramming -- programs that write programs, tactic blocks for example. It is OK if metaprograms aren't completely correct in the sense that the programs they generate will be checked for type correctness by the Lean kernel.

[Scott Morrison]

Indeed, it's easy to prove false inside meta. (It might have been better if there had been several distinct keywords here, separately allowing, e.g. unbounded recursion, and access to metaprogramming, etc, but in Lean 3 they are all lumped together as meta.)

[Mario Carneiro]

In lean 4 they have been separated, into unsafe and partial. partial gives you unbounded recursion and unsafe gives you metaprogramming primitives and other non-pure functions

[Mario Carneiro]

you can prove false with either one, though