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 % \)

Unstable-Funcons-beta : Indexing.cbs | PLAIN | PDF


Value indexing

\[\begin{align*} [ \ \KEY{Entity} \quad & \NAMEREF{value-index} \\ \KEY{Funcon} \quad & \NAMEREF{initialise-index} \\ \KEY{Funcon} \quad & \NAMEREF{allocate-index} \\ \KEY{Funcon} \quad & \NAMEREF{lookup-index} \ ] \end{align*}\]

The following funcons support indexing of values by natural numbers. They could be enhanced to ensure that each value has at most one index, and to allow finding the index of a value.

\[\begin{align*} \KEY{Entity} \quad & \langle \_, \NAMEDECL{value-index}(\_ : \NAMEHYPER{../../../../Funcons-beta/Values}{Value-Types}{ground-values}\STAR) \rangle \TRANS \\& \langle \_, \NAME{value-index}(\_ : \NAME{ground-values}\STAR) \rangle \end{align*}\] \[\begin{align*} \KEY{Funcon} \quad & \NAMEDECL{initialise-index} : \TO \NAMEHYPER{../../../../Funcons-beta/Values/Primitive}{Null}{null-type} \\ \KEY{Rule} \quad & \langle \NAMEREF{initialise-index}, \NAMEREF{value-index} ( \_ ) \rangle \TRANS \langle \NAMEHYPER{../../../../Funcons-beta/Values/Primitive}{Null}{null-value}, \NAMEREF{value-index} ( \ ) \rangle \end{align*}\] \[\begin{align*} \KEY{Funcon} \quad & \NAMEDECL{allocate-index}( \_ : \NAMEHYPER{../../../../Funcons-beta/Values}{Value-Types}{ground-values}) : \TO \NAMEHYPER{../../../../Funcons-beta/Values/Primitive}{Integers}{natural-numbers} \\ \KEY{Rule} \quad & \langle \NAMEREF{allocate-index} ( \VAR{V} : \NAMEHYPER{../../../../Funcons-beta/Values}{Value-Types}{ground-values} ), \NAMEREF{value-index} ( \VAR{V}\STAR ) \rangle \TRANS \\&\quad \langle \NAMEHYPER{../../../../Funcons-beta/Values/Composite}{Sequences}{length} ( \VAR{V}\STAR, \VAR{V} ), \NAMEREF{value-index} ( \VAR{V}\STAR, \VAR{V} ) \rangle \end{align*}\] \[\begin{align*} \KEY{Funcon} \quad & \NAMEDECL{lookup-index}( \_ : \NAMEHYPER{../../../../Funcons-beta/Values/Primitive}{Integers}{natural-numbers}) : \TO \NAMEHYPER{../../../../Funcons-beta/Values}{Value-Types}{ground-values} \\ \KEY{Rule} \quad & \langle \NAMEREF{lookup-index} ( \VAR{N} : \NAMEHYPER{../../../../Funcons-beta/Values/Primitive}{Integers}{natural-numbers} ), \NAMEREF{value-index} ( \VAR{V}\STAR ) \rangle \TRANS \\&\quad \langle \NAMEHYPER{../../../../Funcons-beta/Values/Composite}{Sequences}{index} ( \VAR{N}, \VAR{V}\STAR ), \NAMEREF{value-index} ( \VAR{V}\STAR ) \rangle \\ \KEY{Assert} \quad & \NAMEREF{lookup-index} ( \NAMEREF{allocate-index} ( \VAR{V} : \NAMEHYPER{../../../../Funcons-beta/Values}{Value-Types}{ground-values} ) ) \TRANS \VAR{V} \end{align*}\]