Stream: new members
Topic: Hypothetical judgements
Ariel Davis (Dec 04 2019 at 19:40):
Hello. I'm trying to use Lean to define the semantics of a simple programming language. To do that, I would like to first define inductive types which represent the expressions and types in the language, respectively. I have done this. I would then like to define the judgements for the typing of expressions. This is where I am running into problems. I believe I have something that works for simple expressions, but I'm not sure how to change what i have to account for 'hypotheses' (like 'the variable x has type t'). This is necessary to write down the typing rules for, for instance, an expression "let x = e in e'" where x is a variable and e, e' are expressions. I have attached my code as it is now. Could anyone help me with this? e.lean
Wojciech Nawrocki (Dec 04 2019 at 19:47):
There are many ways to deal with this. One approach is to let the context be a partial map from variables to types. Then extracting a variable is function application and adding
x is extending the map by adding a new case that handles
x. Probably the canonical resource for this is Software Foundations. You would be interested in the section on typing (link), but in general going through the Stlc chapters will explain exactly how to do what you want. Foundations uses Coq, so the Lean code will be a little different, but not by too much.
Rob Lewis (Dec 04 2019 at 19:49):
To start a bit earlier: you'll want to change your
has_typ function to
has_typ_in_ctx. Instead of being a binary relation between a term and a type, it will be a three-way relation between a term, a type, and a context.
Patrick Massot (Dec 04 2019 at 19:50):
I cannot help with this kind of formalization, but I have a practical suggestion. People here usually post their Lean code either in their message when it is short enough or using https://gist.github.com/ or a similar website. We don't want people to get used to opening a Lean file randomly downloaded from the internet into VSCode (or emacs) without seeing its content first, since this is a huge security hole (VScode will start running Lean on that file without letting you inspect its content first).
Rob Lewis (Dec 04 2019 at 19:50):
You'll need to choose how to represent contexts. There are many possibilities here.
Rob Lewis (Dec 04 2019 at 19:50):
Wojciech's suggestion of a partial map makes sense, but another simple one (good enough to write down a basic sketch, at least) would be
@[reducible] def context : Type := list (exp × typ)
Rob Lewis (Dec 04 2019 at 19:51):
So you could do something like
inductive has_typ: context → exp -> typ -> Prop -- 0 : nat | z: ∀ ctx, has_typ ctx exp.z typ.num -- e : nat => Succ(e) : nat | succ (e: exp) (ctx : context) (_: has_typ ctx e typ.num): has_typ ctx (exp.succ e) typ.num -- true : bool | t: ∀ ctx, has_typ ctx exp.t typ.bool -- false : bool | f: ∀ ctx, has_typ ctx exp.f typ.bool -- Γ, x : τ ⊢ x : τ | id (x : exp) (τ : typ) (ctx : context) : (x, τ) ∈ ctx → has_typ ctx x τ -- Γ ⊢ e : τ ∧ Γ, x : τ ⊢ e' : τ' => Γ ⊢ let x = e in e' : τ' -- ???
Rob Lewis (Dec 04 2019 at 19:52):
I've left the last one for you to think about.
Ariel Davis (Dec 04 2019 at 19:52):
Thanks everyone for the responses. @Patrick Massot sorry, i hadn't considered that. I'll be more careful in the future.
Patrick Massot (Dec 04 2019 at 19:53):
Rob Lewis (Dec 04 2019 at 19:56):
We don't want people to get used to opening a Lean file randomly downloaded from the internet into VSCode (or emacs) without seeing its content first
For the record, this one is safe, and I did check first :wink:
Rob Lewis (Dec 04 2019 at 19:58):
Unrelated, why does Zulip highlight the word
context? Was that ever a keyword?
Last updated: May 06 2021 at 22:13 UTC