「SF-LC」8 Maps
useful as env
Map == Dictionary
- building data structure.
- use of reflection to streamline proofs.
Two flavors of maps:
- total maps, return default when lookup fails
- partial maps, return
option
to indicate success/failure, usingNone
as the default.
The Coq Standard Lib
From now on, importing from std lib. (but should not notice much difference)
1 | From Coq Require Import Arith.Arith. |
TODO: what’s the differences above?
Answered in Coq Intensive:
Require
give access but need to use qualified nameImport
no need to use qualified nameExport
module importing me no need to use qualified name as well
String
in Coq is list
of Char
and Char
is record of 8 Bool
…
Identifiers
we need a type for the keys that we use to index into our maps.
In Lists.v
(Partial Maps):
1 | Inductive id : Type := |
From now on we will use the string
from Coq’s std lib:
1 | Definition eqb_string (x y : string) : bool := |
The equality check fn for string
from stdlib is string_des
, which returns a sumbool
type, i.e. {x=y} + {x≠y}
.
which can be thought of as an “evidence-carrying boolean”.
Formally, an element ofsumbool
is either or
- a proof that two things are equal
- a proof that they are unequal,
together with a tag indicating which.
Some properties:
1 | (* reflexive relation *) |
Total Maps
use functions, rather than lists of key-value pairs, to build maps.
The advantage of this representation is that it offers a more extensional view of maps. 外延性(where two maps that respond to queries in the same way will be represented as literally the same thing rather than just “equivalent” data structures. This, in turn, simplifies proofs that use maps.)
1 | Definition total_map (A : Type) := string -> A. |
Where is the data stored? Closure!
My Reviews on API style of ML
1 | Definition examplemap := |
since t_update
is defined as so called “t-first” style.
Reason/BuckleScript and OCaml stdlib uses this style as well:
1 | let examplemap = |
1 | val add : key -> 'a -> 'a t -> 'a t |
Or, In Jane Street “named-argument” style
e.g. Real World OCaml
1 | let examplemap = |
Lightweight Meta-Programming in Coq - Notation
In Coq, we can leverage some meta programming:
1 | Notation "'_' '!->' v" := (t_empty v) |
Noticed that the “Map building” is in a reversed order…
Note that we don’t need to define a find operation because it is just function application!
1 | Example update_example2 : examplemap' "foo" = true. |
Partial Maps
we define partial maps on top of total maps.
A partial map with elements of typeA
is simply a total map with elements of typeoption A
and default elementNone
.
1 | Definition partial_map (A : Type) := total_map (option A). |
we use the “standard” map operator ↦
for partial map since maps in CS are usually partial.
Maps are functions#Maps_as_functions)
In many branches of mathematics, the term map is used to mean a function.
partial map = partial function,
total map = total function.In category theory, “map” is often used as a synonym for morphism or arrow.
In formal logic, “map” is sometimes used for a functional symbol.