Link Search Menu Expand Document
\( % cbs-katex.sty % \newcommand{\STYLE}[2]{\htmlClass{cbs-#1}{#2}} \newcommand{\DECL}[3]{\htmlId{#1:#2}{#3}} \newcommand{\REF}[3]{\href{###1:#2}{#3}} \newcommand{\HYPER}[5]{\href{#1/#2/index.html###3:#4}{#5}} % \SHADE{MATH} can be defined to produce a shaded background to highlight % inline MATH in running text: \newcommand{\SHADE}[1]{#1} % \KEY{TEXT}, \STRING{TEXT}, \ATOM{TEXT}, \LEX{TEXT} can be used in math mode: \newcommand{\KEY}[1]{\textsf{\textit{\STYLE{Key}{#1}}}} \newcommand{\STRING}[1]{\textsf{``\texttt{#1}''}} \newcommand{\ATOM}[1]{\textsf{`\texttt{#1}'}} \newcommand{\LEX}[1]{\textsf{\STYLE{Key}{`}\texttt{#1}\STYLE{Key}{'}}} % The following commands produce ASCII characters that are treated specially by LaTeX: \newcommand{\HASH}{\char`\#} \newcommand{\DOLLAR}{\char`\$} \newcommand{\PERCENT}{\char`\%} \newcommand{\AMPERSAND}{\char`\&} \newcommand{\APOSTROPHE}{\char`\'} \newcommand{\BACKSLASH}{\char`\\} \newcommand{\CARET}{\char`\^} \newcommand{\UNDERSCORE}{\char`\_} \newcommand{\GRAVE}{\char`\`} \newcommand{\LEFTBRACE}{\char`\{} \newcommand{\RIGHTBRACE}{\char`\}} \newcommand{\TILDE}{\textasciitilde} % {\char`\~} % \NAME{name} highlights the name; % \NAMEDECL{name} declares Name.name as the target of links to name; % \NAMEREF{name} links name to the target Name.name in the current file; % \NAMEHYPER{url}{file}{name} links name to Name.name at url/file/file.pdf. % Similarly for \VAR{partvariable}, \SYN{syntaxname}, \SEM{semanticsName}, % and \SECT{sectionnumber} % The kerns in \SUB and \VAR avoid overlaps with primes: \newcommand{\SUB}[1]{_{\kern-2mu\STYLE{PartVariable}{\textsf{#1}}}} % PLAIN \newcommand{\VAR}[1]{\STYLE{PartVariable}{\textsf{\textit{#1}\kern2mu}}} \newcommand{\NAME}[1]{\STYLE{Name}{\textsf{#1}}} \newcommand{\SYN}[1]{\STYLE{SyntaxName}{\textsf{#1}}} \newcommand{\SEM}[1]{\STYLE{SemanticsName}{\textsf{#1}}} \newcommand{\SECT}[1]{\STYLE{SectionNumber}{\textsf{#1}}} % DECL \newcommand{\VARDECL}[1]{\DECL{PartVariable}{#1}{\VAR{#1}}} \newcommand{\NAMEDECL}[1]{\DECL{Name}{#1}{\NAME{#1}}} \newcommand{\SYNDECL}[1]{\DECL{SyntaxName}{#1}{\SYN{#1}}} \newcommand{\SEMDECL}[1]{\DECL{SemanticsName}{#1}{\SEM{#1}}} \newcommand{\SECTDECL}[1]{\DECL{SectionNumber}{#1}{\textsf{#1}}} % REF \newcommand{\VARREF}[1]{\REF{PartVariable}{#1}{\VAR{#1}}} \newcommand{\NAMEREF}[1]{\REF{Name}{#1}{\NAME{#1}}} \newcommand{\SYNREF}[1]{\REF{SyntaxName}{#1}{\SYN{#1}}} \newcommand{\SEMREF}[1]{\REF{SemanticsName}{#1}{\SEM{#1}}} \newcommand{\SECTREF}[1]{\REF{SectionNumber}{#1}{\SECT{#1}}} % HYPER \newcommand{\VARHYPER}[3]{\HYPER{#1}{#2}{PartVariable}{#3}{\VAR{#3}}} \newcommand{\NAMEHYPER}[3]{\HYPER{#1}{#2}{Name}{#3}{\NAME{#3}}} \newcommand{\SYNHYPER}[3]{\HYPER{#1}{#2}{SyntaxName}{#3}{\SYN{#3}}} \newcommand{\SEMHYPER}[3]{\HYPER{#1}{#2}{SemanticsName}{#3}{\SEM{#3}}} \newcommand{\SECTHYPER}[3]{\HYPER{#1}{#2}{SectionNumber}{#3}{\SECT{#3}}} % \LEFTPHRASE MATH \RIGHTPHRASE produces [[ MATH ]] with proper brackets: \newcommand{\LEFTPHRASE}{\llbracket} \newcommand{\RIGHTPHRASE}{\rrbracket} % \LEFTGROUP MATH \RIGHTGROUP produces ( MATH ) where the parentheses are % highlighted the same as keywords: \newcommand{\LEFTGROUP}{\STYLE{Key}{(}} \newcommand{\RIGHTGROUP}{\STYLE{Key}{)}} % MATH\PLUS produces a superscript + % MATH\STAR produces a superscript * % MATH\QUERY produces a superscript ? \newcommand{\PLUS}{{}^{\texttt{+}}} \newcommand{\STAR}{{}^{\texttt{*}}} \newcommand{\QUERY}{{}^{\texttt{?}}} % \RULE{& PREMISE \\ & ...}{& FORMULA ... \\ & ...} produces an inference rule % with separately aligned premises and conclusion % PREMISE % ... % ----------- % FORMULA ... % ... \newcommand{\RULE}[2] {\frac{\begin{aligned}#1\end{aligned}}{\begin{aligned}#2\end{aligned}}} % \AXIOM{& FORMULA ... \\ & ...} produces an aligned formula % % FORMULA ... % ... \newcommand{\AXIOM}[1]{\begin{aligned}#1\end{aligned}} % \TO TYPE produces => TYPE \newcommand{\TO}{\mathop{\Rightarrow}} % TERM \TRANS TERM produces TERM ---> TERM \newcommand{\TRANS}{\longrightarrow} % TERM \xrightarrow{LABEL} TERM puts the label above the long arrow % \)

Funcons-beta : Maps.cbs | PLAIN | PDF


Maps

\[\begin{align*} [ \ \KEY{Type} \quad & \NAMEREF{maps} \\ \KEY{Funcon} \quad & \NAMEREF{map} \\ \KEY{Funcon} \quad & \NAMEREF{map-elements} \\ \KEY{Funcon} \quad & \NAMEREF{map-lookup} \\ \KEY{Alias} \quad & \NAMEREF{lookup} \\ \KEY{Funcon} \quad & \NAMEREF{map-domain} \\ \KEY{Alias} \quad & \NAMEREF{dom} \\ \KEY{Funcon} \quad & \NAMEREF{map-override} \\ \KEY{Funcon} \quad & \NAMEREF{map-unite} \\ \KEY{Funcon} \quad & \NAMEREF{map-delete} \ ] \end{align*}\] \[\begin{align*} \KEY{Meta-variables} \quad & \VAR{GT} <: \NAMEHYPER{../..}{Value-Types}{ground-values} \qquad \\& \VAR{T}\QUERY <: \NAMEHYPER{../..}{Value-Types}{values}\QUERY \end{align*}\] \[\begin{align*} \KEY{Built-in Type} \quad & \NAMEDECL{maps}( \VAR{GT} , \VAR{T}\QUERY ) \end{align*}\]

\(\SHADE{\NAMEREF{maps} ( \VAR{GT}, \VAR{T}\QUERY )}\) is the type of possibly-empty finite maps from values of type \(\SHADE{\VAR{GT}}\) to optional values of type \(\SHADE{\VAR{T}\QUERY}\).

\[\begin{align*} \KEY{Built-in Funcon} \quad & \NAMEDECL{map}( \_ : ( \NAMEHYPER{../.}{Tuples}{tuples} ( \VAR{GT}, \VAR{T}\QUERY ) )\STAR) : \TO ( \NAMEREF{maps} ( \VAR{GT}, \VAR{T}\QUERY ) )\QUERY \end{align*}\]

\(\SHADE{\NAMEREF{map} ( \NAMEHYPER{../.}{Tuples}{tuple} ( \VAR{K}\SUB{1}, \VAR{V}\SUB{1}\QUERY ), \cdots, \NAMEHYPER{../.}{Tuples}{tuple} ( \VAR{K}\SUB{n}, \VAR{V}\SUB{n}\QUERY ) )}\) constructs a map from \(\SHADE{\VAR{K}\SUB{1}}\) to \(\SHADE{\VAR{V}\SUB{1}\QUERY}\), …, \(\SHADE{\VAR{K}\SUB{n}}\) to \(\SHADE{\VAR{V}\SUB{n}\QUERY}\), provided that \(\SHADE{\VAR{K}\SUB{1}}\), …, \(\SHADE{\VAR{K}\SUB{n}}\) are distinct, otherwise the result is \(\SHADE{( \ )}\).

Note that \(\SHADE{\NAMEREF{map} ( \cdots )}\) is not a constructor operation.

The built-in notation \(\SHADE{\{ \VAR{K}\SUB{1} \mapsto \VAR{V}\SUB{1}\QUERY, \cdots, \VAR{K}\SUB{n} \mapsto \VAR{V}\SUB{n}\QUERY \}}\) is equivalent to \(\SHADE{\NAMEREF{map} ( \NAMEHYPER{../.}{Tuples}{tuple} ( \VAR{K}\SUB{1}, \VAR{V}\SUB{1}\QUERY ), \cdots, \NAMEHYPER{../.}{Tuples}{tuple} ( \VAR{K}\SUB{n}, \VAR{V}\SUB{n}\QUERY ) )}\). Note however that in general, maps cannot be identified with sets of tuples, since the values \(\SHADE{\VAR{V}\SUB{i}\QUERY}\) are not restricted to \(\SHADE{\NAMEHYPER{../..}{Value-Types}{ground-values}}\).

When \(\SHADE{\VAR{T}\QUERY <: \NAMEHYPER{../..}{Value-Types}{types}}\), \(\SHADE{\NAMEREF{maps} ( \VAR{GT}, \VAR{T}\QUERY ) <: \NAMEHYPER{../..}{Value-Types}{types}}\). The type \(\SHADE{\VAR{MT} : \NAMEREF{maps} ( \VAR{GT}, \VAR{T}\QUERY )}\) represents the set of value-maps \(\SHADE{\VAR{MV} : \NAMEREF{maps} ( \VAR{GT}, \NAMEHYPER{../..}{Value-Types}{values}\QUERY )}\) such that \(\SHADE{\NAMEREF{dom} ( \VAR{MV} )}\) is a subset of \(\SHADE{\NAMEREF{dom} ( \VAR{MT} )}\) and for all \(\SHADE{\VAR{K}}\) in \(\SHADE{\NAMEREF{dom} ( \VAR{MV} )}\), \(\SHADE{ \NAMEREF{map-lookup} ( \VAR{MV}, \VAR{K} ) : \NAMEREF{map-lookup} ( \VAR{MT}, \VAR{K} )}\).

\[\begin{align*} \KEY{Built-in Funcon} \quad & \NAMEDECL{map-elements}( \_ : \NAMEREF{maps} ( \VAR{GT}, \VAR{T}\QUERY )) : \TO ( \NAMEHYPER{../.}{Tuples}{tuples} ( \VAR{GT}, \VAR{T}\QUERY ) )\STAR \end{align*}\]

The sequence of tuples \(\SHADE{( \NAMEHYPER{../.}{Tuples}{tuple} ( \VAR{K}\SUB{1}, \VAR{V}\SUB{1}\QUERY ), \cdots, \NAMEHYPER{../.}{Tuples}{tuple} ( \VAR{K}\SUB{n}, \VAR{V}\SUB{n}\QUERY ) )}\) given by \(\SHADE{\NAMEREF{map-elements} ( \VAR{M} )}\) contains each mapped value \(\SHADE{\VAR{K}\SUB{i}}\) just once. The order of the elements is unspecified, and may vary between maps.

\[\begin{align*} \KEY{Assert} \quad & \NAMEREF{map} ( \NAMEREF{map-elements} ( \VAR{M} ) ) == \VAR{M} \end{align*}\] \[\begin{align*} \KEY{Built-in Funcon} \quad & \NAMEDECL{map-lookup}( \_ : \NAMEREF{maps} ( \VAR{GT}, \VAR{T}\QUERY ), \VAR{K} : \VAR{GT}) : \TO ( \VAR{T}\QUERY )\QUERY \\ \KEY{Alias} \quad & \NAMEDECL{lookup} = \NAMEREF{map-lookup} \end{align*}\]

\(\SHADE{\NAMEREF{map-lookup} ( \VAR{M}, \VAR{K} )}\) gives the optional value to which \(\SHADE{\VAR{K}}\) is mapped by \(\SHADE{\VAR{M}}\), if any, and otherwise \(\SHADE{( \ )}\).

\[\begin{align*} \KEY{Built-in Funcon} \quad & \NAMEDECL{map-domain}( \_ : \NAMEREF{maps} ( \VAR{GT}, \VAR{T}\QUERY )) : \TO \NAMEHYPER{../.}{Sets}{sets} ( \VAR{GT} ) \\ \KEY{Alias} \quad & \NAMEDECL{dom} = \NAMEREF{map-domain} \end{align*}\]

\(\SHADE{\NAMEREF{map-domain} ( \VAR{M} )}\) gives the set of values mapped by \(\SHADE{\VAR{M}}\).

\(\SHADE{\NAMEREF{map-lookup} ( \VAR{M}, \VAR{K} )}\) is always \(\SHADE{( \ )}\) when \(\SHADE{\VAR{K}}\) is not in \(\SHADE{\NAMEREF{map-domain} ( \VAR{M} )}\).

\[\begin{align*} \KEY{Built-in Funcon} \quad & \NAMEDECL{map-override}( \_ : ( \NAMEREF{maps} ( \VAR{GT}, \VAR{T}\QUERY ) )\STAR) : \TO \NAMEREF{maps} ( \VAR{GT}, \VAR{T}\QUERY ) \end{align*}\]

\(\SHADE{\NAMEREF{map-override} ( \cdots )}\) takes a sequence of maps. It returns the map whose domain is the union of their domains, and which maps each of those values to the same optional value as the first map in the sequence in whose domain it occurs . When the domains of the \(\SHADE{\VAR{M}\STAR}\) are disjoint, \(\SHADE{\NAMEREF{map-override} ( \VAR{M}\STAR )}\) is equivalent to \(\SHADE{\NAMEREF{map-unite} ( \VAR{M}\STAR )}\).

\[\begin{align*} \KEY{Built-in Funcon} \quad & \NAMEDECL{map-unite}( \_ : ( \NAMEREF{maps} ( \VAR{GT}, \VAR{T}\QUERY ) )\STAR) : \TO ( \NAMEREF{maps} ( \VAR{GT}, \VAR{T}\QUERY ) )\QUERY \end{align*}\]

\(\SHADE{\NAMEREF{map-unite} ( \cdots )}\) takes a sequence of maps. It returns the map whose domain is the union of their domains, and which maps each of those values to the same optional value as the map in the sequence in whose domain it occurs, provided that those domains are disjoint - otherwise the result is \(\SHADE{( \ )}\).

\[\begin{align*} \KEY{Built-in Funcon} \quad & \NAMEDECL{map-delete}( \_ : \NAMEREF{maps} ( \VAR{GT}, \VAR{T}\QUERY ), \_ : \NAMEHYPER{../.}{Sets}{sets} ( \VAR{GT} )) : \TO \NAMEREF{maps} ( \VAR{GT}, \VAR{T}\QUERY ) \end{align*}\]

\(\SHADE{\NAMEREF{map-delete} ( \VAR{M}, \VAR{S} )}\) takes a map \(\SHADE{\VAR{M}}\) and a set of values \(\SHADE{\VAR{S}}\), and returns the map obtained from \(\SHADE{\VAR{M}}\) by removing \(\SHADE{\VAR{S}}\) from its domain.

\[\begin{align*} \KEY{Assert} \quad & \NAMEREF{map-domain} ( \NAMEREF{map-delete} ( \VAR{M}, \VAR{S} ) ) == \NAMEHYPER{../.}{Sets}{set-difference} ( \NAMEREF{map-domain} ( \VAR{M} ), \VAR{S} ) \end{align*}\]