# Zulip Chat Archive

## Stream: new members

### Topic: Nondeterminism and Meta

#### Logan Murphy (Sep 05 2020 at 20:01):

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 (Sep 05 2020 at 20:11):

`meta`

means "don't check if the recursion terminates"

#### Kyle Miller (Sep 05 2020 at 20:33):

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 (Sep 06 2020 at 04:40):

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 (Sep 06 2020 at 05:09):

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 (Sep 06 2020 at 05:09):

you can prove false with either one, though

Last updated: May 11 2021 at 12:15 UTC