Zulip Chat Archive

Stream: new members

Topic: Nondeterminism and Meta


view this post on Zulip 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

view this post on Zulip Kenny Lau (Sep 05 2020 at 20:11):

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

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip 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

view this post on Zulip 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