# Zulip Chat Archive

## Stream: new members

### Topic: do i have to prove a deterministic lemma and a final lemma?

#### Huỳnh Trần Khanh (Jun 10 2021 at 04:54):

the LoVe repository states that i should prove these two lemmas to make sure that my machine model is sane—why?

#### Huỳnh Trần Khanh (Jun 10 2021 at 04:54):

https://github.com/blanchette/logical_verification_2020/blob/master/lean/love08_operational_semantics_demo.lean#L475 https://github.com/blanchette/logical_verification_2020/blob/master/lean/love08_operational_semantics_demo.lean#L429

#### Huỳnh Trần Khanh (Jun 10 2021 at 04:57):

alright off for lunch! i'll read your responses later

#### Mario Carneiro (Jun 10 2021 at 06:38):

You don't have to prove a determinism lemma, but it is good to do so if your semantics is deterministic because it is easier to reason with a deterministic semantics

#### Mario Carneiro (Jun 10 2021 at 06:39):

you can conceptualize a deterministic state function as a sequence of steps in a line

#### Mario Carneiro (Jun 10 2021 at 06:40):

a nondeterministic state function has a tree of steps, so when you talk about eventually reaching some state you have to be careful about whether you mean that all paths through the tree end in a terminal state, or just one does, or for every node in the tree there exists a path to some terminal state

#### Mario Carneiro (Jun 10 2021 at 06:42):

the second theorem is often not true; a state which does not step but is also not a final state is called a stuck state and usually indicates some kind of error condition. The normal way this theorem is stated is that *if* some typing condition on the program holds, *then* the corresponding machine state is not stuck, and it is called the "progress lemma"

Last updated: Dec 20 2023 at 11:08 UTC