Generic State

Stream: Program verification

[Ian Riley]

This may have been asked before, but I'm reading through Hitchhiker's Guide to Logical Verification, and I'm curious how I might define a state that's more generic than the natural numbers. It seems like one approach would be something like def state: Type := string -> Type. I've also considered def state {t : Type} : Type := string -> t if that's possible. Has anyone approached this problem?

[Marcus Rossel]

What do you mean by "state" in this context?
Perhaps you're looking for docs#sigma?

[Anne Baanen]

I assume you're referring to a state in the semantics of the While language, right? Then indeed def state := string → Σ (t : Type), t could work. Each variable has its own type at each point in time.

[Ian Riley]

Marcus Rossel said:

What do you mean by "state" in this context?
Perhaps you're looking for docs#sigma?

In the guide, state is used as a definition to reason over the values of program variables. The book defines state as ‘def state : Type := string -> Nat’ so variables can only be given unsigned int values or enums. I was hoping to define state so that I could reason over variables having any type as their assigned value even to the point of being able to assign structured types or inductive types.

[Ian Riley]

Anne Baanen said:

I assume you're referring to a state in the semantics of the While language, right? Then indeed def state := string → Σ (t : Type), t could work. Each variable has its own type at each point in time.

That’s right. So what does the sigma do in this context? Edit: is it just shorthand for creating a dependent type with one arg?

[Anne Baanen]

The Sigma type contains dependent pairs: (x : α, y : β x) where the type of y is allowed to depend on x. In this case, the type of y is exactly equal to x.

[Anne Baanen]

So it is indeed shorthand for a specific dependent type, but there are many more dependent types available, such as Pi types (dependent functions).

[Ian Riley]

I’ve read about sigma and pi in Lean 3. I assume that they still work the same in lean 4? In lean 3, they always seemed about the same to me. If sigma is generalizing over Cartesian products and pi over functions, then couldn’t any product be rewritten as an equivalent function? So couldn’t any sigma just be a pi?

[Anne Baanen]

Yes, sigma and pi are core to Lean's type theory and should work the same in Lean 3 and 4 except for minor syntactical changes.

[Anne Baanen]

One way you can intuitively distinguish sigma and pi is that an element of Σ (x : α), β x gives only one tuple, while an element of Π (x : α), β x gives one tuple per element of α. So if α is nonempty and β x is empty for some x, we still have elements of Σ (x : α), β x but there can't be an element of Π (x : α), β x.

[Anne Baanen]

Conversely, if α is empty then there is no element of Σ (x : α), β x while Π (x : α), β x has exactly one element, that maps nothing to doesn't matter.

[Kyle Miller]

It's nice how it works out that card (Σ (x : α), β x) = Σ (x : α), card (β x) and card (Π (x : α), β x) = Π (x : α), card (β x), where on the left-hand sides you have cardinalities of sigma/pi types, and on the right you have sums/products of cardinalies.

One thing to watch out for is that sigma types are a sort of generalization of the cartesian product of a pair of types in a specific order (so the second can depend on the first), but the pi type is the cartesian family of an indexed family of types (and none can depend on one another). I found it to be useful to think about how when you have a non-dependent sigma type, card (Σ (x : α), β) = card α * card β since you're summing up card α copies of card β.

[Kyle Miller]

Many basic combinatorial situations you'd find in an introductory combinatorics class can be modeled with sigma types and pi types. Sigma types are for making sequential choices ("choose an element x of α and then choose an element of β x"), and pi types are for making parallel choices ("for every x in α, choose an element of β x).

[Ian Riley]

Anne Baanen said:

One way you can intuitively distinguish sigma and pi is that an element of Σ (x : α), β x gives only one tuple, while an element of Π (x : α), β x gives one tuple per element of α. So if α is nonempty and β x is empty for some x, we still have elements of Σ (x : α), β x but there can't be an element of Π (x : α), β x.

And this is because Pi being a generalization over functions in lean also means that it's a generalization over total functions?

[Ian Riley]

The state notation with Sigma is actually quite nice. example (s : State) : s{"x" ↦ ⟨Nat, 0⟩} "x" = ⟨Nat, 0⟩ := by state_apply The constructor for the Sigma type makes for very clean examples.

[Anne Baanen]

Ian Riley said:

And this is because Pi being a generalization over functions in lean also means that it's a generalization over total functions?

Yes, precisely! I've become so used to it that I forget that there are non-total functions :)

[Ian Riley]

Thanks! That's been really helpful :)