Modeling of dictionaries and partial functions

Stream: new members

[Relyth]

Hello all. I am a novice at using Lean and interactive proof assistants in general, so apologies if this question is too simple.

I am trying to model the semantics of a simple imperative programming language in Lean 4. This language has a notion of memory which is a map (in the sense of dictionary) that relates a series of variable names (just strings) to values. The issue is that this map is only defined for a subset of variable names that are "in scope", i.e., the memory is a partial function from strings to values.

I am not sure how to model this in the way that is the most amenable for later proofs. A perhaps naïve approach would be to define the memory as a total function from strings to an optional value (i.e.,String -> Option Value). While this works, it seems annoying because in most of the proofs I expect to just assume that any variable names I fix are in scope, so this style would force me to "branch out" every time I try to access the value of a variable in memory, forcing me to seek a contradiction to rule out that branch as impossible. I have been thinking that maybe a better way to do this would be to mimic Array.getby asking for a proof that the variable is defined as an additional argument to the variable lookup operator.

What do you think is the best way to proceed? How would you model this? Thank you very much!

[Chris Bailey]

If your model is functional (something like (program, state) -> state), you can implement a relational model (program, state) -> state -> Prop, which solves this problem by just not permitting a step for a bad lookup. The hitchhikers guide and software foundations vol. 1 have chapters about making and comparing/contrasting functional vs. relational models for PL semantics.

[Relyth]

Thank you very much for sharing that resource, it looks very useful!