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