From 2b5ffb0d2ef3820e98598b58b927bb695c907ed6 Mon Sep 17 00:00:00 2001 From: Quinn Dougherty Date: Wed, 30 Mar 2022 12:00:47 -0400 Subject: [PATCH] functions with sugars, base types --- spec/src/introduction.tex | 2 + spec/src/main.tex | 9 +-- spec/src/semantics.tex | 2 +- spec/src/syntax.tex | 117 ++++++++++++++++++++++++++++++++++++-- 4 files changed, 120 insertions(+), 10 deletions(-) diff --git a/spec/src/introduction.tex b/spec/src/introduction.tex index bc018927..d4c8375a 100644 --- a/spec/src/introduction.tex +++ b/spec/src/introduction.tex @@ -4,6 +4,8 @@ The current document is a formal description of the syntax that Squiggle will target in it's alpha release, scheduled for Q3 2022. It is initially drafted for consumption by the team, not by the user base. +Note that the document is prescriptive rather than descriptive. + For an informal story of what we are about to see, consult \cite{@SqgCodePlan}. We proceed by a BNF (\cite{@BNFWiki}), and take nods about how to communicate about programming languages from \cite{@CraftingInterpreters, Appendix I}, neglecting lessons from \cite{@PFPL}. diff --git a/spec/src/main.tex b/spec/src/main.tex index 3ae6d679..521985e4 100644 --- a/spec/src/main.tex +++ b/spec/src/main.tex @@ -3,19 +3,20 @@ \usepackage{syntax} \setlength{\grammarparsep}{2ex plus 0.1ex minus 0.05ex} % \usepackage[T1]{fontenc} -\usepackage{bussproofs} +% \usepackage{bussproofs} \usepackage{amsfonts} \usepackage{subfiles} +\usepackage{datetime} \usepackage{hyperref} -\hypersetup{colorlinks = true, citecolor = blue} +\hypersetup{colorlinks=true, citecolor=blue} \usepackage[backend=biber, hyperref=true, citestyle=authoryear]{biblatex} \addbibresource{biblio.bib} \title{Squiggle $\alpha$-v0.1 Specification (INTERNAL)} -\author{Quinn Dougherty} -\date{April 2022} +\author{Quinn Dougherty - \texttt{quinn@quantifieduncertainty.org}} +\date{This render: \today} \begin{document} \maketitle{} diff --git a/spec/src/semantics.tex b/spec/src/semantics.tex index a1c99e98..8856f0f3 100644 --- a/spec/src/semantics.tex +++ b/spec/src/semantics.tex @@ -2,6 +2,6 @@ \begin{document} \section{Semantics}\label{section:semantics} -TODO: Some way of expressing the evaluation and execution model. +\textbf{TODO: Operational semantics}. \end{document} diff --git a/spec/src/syntax.tex b/spec/src/syntax.tex index 70892f82..ed422ae1 100644 --- a/spec/src/syntax.tex +++ b/spec/src/syntax.tex @@ -2,6 +2,18 @@ \begin{document} \section{Syntax}\label{section:syntax} +\subsection{Lexical descriptions of constants and variables} +The lexical grammars of \texttt{float} and $\langle \textit{var} \rangle$ are given by the following regular expressions (floats from \cite{@CraftingInterpreters, Appendix I}) + +\begin{tabular}{ c c } + \texttt{float} & $\langle digit \rangle$+ ( . $\langle digit \rangle$+ )? \\ + $\langle digit \rangle$ & 0-9 \\ + $\langle var \rangle$ & a-zA-Z+ a-zA-Z0-9? +\end{tabular}\label{regex:float} + + +\subsection{A high-level story} + Details about assignment and arithmetic on floats will follow eventually, but I want to sketch out a theory of combining distributions, first. Abstractly, you can think of Squiggle as containing two types @@ -9,25 +21,120 @@ Abstractly, you can think of Squiggle as containing two types ::= \alt \texttt{float} \end{grammar}\label{gram:type} + +\textbf{Squiggle does not support integers}. Every number is cast to float if it is not specified with a trailing \texttt{.0}. + Where \texttt{float} is ordinary IEEE754 floating point numbers, and $\langle \textit{GenericDist} \rangle$ is as follows \begin{grammar} ::= \alt \texttt{SampleSet} \alt - ::= \alt \alt + ::= \texttt{Mixed} \alt \texttt{Continuous} \alt \texttt{Discrete} ::= \texttt{Normal} \alt \texttt{LogNormal} \alt \texttt{Triangular} \alt \texttt{Beta} \alt \texttt{Uniform} \alt \texttt{Float} \alt \texttt{Exponential} \alt \texttt{Cauchy} -\end{grammar} +\end{grammar}\label{gram:gendist} From a grammatical perspective \texttt{SampleSet} and all of the alternatives of $\langle \textit{Symbolic} \rangle$ are \textit{black boxes}. They needn't be discussed from this point of view. -Finally, most of the magic happens in $\langle \textit{Expression} \rangle$ +Finally, most of the magic happens in $\langle \textit{Expression} \rangle$, though this story is suppresses a lot of the detail that would make opertational semantics possible. \begin{grammar} - ::= \alt \texttt{float} \alt * \alt .* + ::= \alt \texttt{float} \alt list() \alt \alt * \alt .* \alt ./ - ::= + \alt .+ + ::= \alt + \alt .+ \alt - \alt .- +\end{grammar}\label{gram:expr} + +In the true story, these binary operators shall be revealed to be \textit{sugars}, with different meanings depending on if their arguments are $\langle \textit{GenericDist} \rangle$ or \texttt{float}. + +\subsection{Functions} + +We have a type of not-necessarily-normalized distributions along with a normalization function \texttt{normalize}, where an ordinary $\langle \textit{GenericDist} \rangle$ corresponds to the special case where \texttt{normalize} is idempotent. + +Give another alternative to $\langle \textit{GenericDist} \rangle$ for the normalization function, and define a list of functions that return $\langle \textit{NonNormalizedDist} \rangle$ +\begin{grammar} + ::= \alt \texttt{normalize}\ + + ::= + + \alt \texttt{distFloatAdd} \texttt{float} + \alt \texttt{distFloatMultiply} \texttt{float} + \alt \texttt{distFloatSubtract} \texttt{float} + \alt \texttt{distFloatDivide} \texttt{float} + \alt \texttt{distFloatExponent} \texttt{float} + \alt \texttt{pointwiseAddConstant} \texttt{float} + \alt \texttt{pointwiseMultiplyConstant} \texttt{float} + \alt \texttt{pointwiseSubtractConstant} \texttt{float} + \alt \texttt{pointwiseDivideConstant} \texttt{float} + \alt \texttt{pointwiseLogConstant} \texttt{float} + \alt \texttt{distDistAdd} + \alt \texttt{distDistSum} list() + \alt \texttt{distDistMultiply} + \alt \texttt{distDistProduct} list() + \alt \texttt{distDistSubtract} + \alt \texttt{distDistDivide} + \alt \texttt{distDistExponent} + \alt \texttt{pointwiseDistAdd} + \alt \texttt{pointwiseDistSum} list() + \alt \texttt{pointwiseDistMultiply} + \alt \texttt{pointwiseDistProduct} list() + \alt \texttt{pointwiseDistSubtract} + \alt \texttt{pointwiseDistDivide} + \alt \texttt{pointwiseDistExponent} + \alt \texttt{truncate} \texttt{float} \texttt{float} + \alt \texttt{truncateLeft} \texttt{float} + \alt \texttt{truncateRight} \texttt{float} +\end{grammar}\label{gram:nonnormdist} + +Note, \texttt{pointwiseFloat*} and \texttt{pointwise*Constant} are each simple dispatchers that cast the float to a constant distribution (a uniform distribution with one outcome) then call the corresponding \texttt{distDist*} or \texttt{pointwiseDist*} function. + +\textbf{TODO: We'll get rid of the NonNormalizedDist -> float -> NonNormalizedDist and cast float to dist at operatingtime}. + +We have basic arithmetic on floats along with functions from dist to float. +\begin{grammar} + ::= + \texttt{float} + \alt \texttt{add} \texttt{float} \texttt{float} + \alt \texttt{multiply} \texttt{float} \texttt{float} + \alt \texttt{subtract} \texttt{float} \texttt{float} + \alt \texttt{divide} \texttt{float} \texttt{float} + \alt \texttt{exponent} \texttt{float} \texttt{float} + \alt \texttt{log} \texttt{float} \texttt{float} + \alt \texttt{pdfPoint} \texttt{float} + \alt \texttt{invPdfPoint} \texttt{float} + \alt \texttt{cdfPoint} \texttt{float} + \alt \texttt{mean} + \alt \texttt{sample} +\end{grammar}\label{gram:float} + +\textbf{TODO: can we have log on floats?} +\textbf{TODO: We may be cutting nSamples from alpha because we don't want to deal with ints at all.} + +\subsubsection{Sugars/operators} +\begin{tabular}{ c c } + \texttt{distDistAdd} & \texttt{+} \\ + \texttt{distDistMultiply} & \texttt{*} \\ + \texttt{distDistSubtract} & \texttt{-} \\ + \texttt{distDistDivide} & \texttt{/} \\ + \texttt{distDistExponent} & \texttt{**} \\ + \texttt{pointwiseDistAdd} & \texttt{.+} \\ + \texttt{distDistMultiply} & \texttt{.*} \\ + \texttt{distDistSubtract} & \texttt{.-} \\ + \texttt{distDistDivide} & \texttt{./} \\ + \texttt{distDistExponent} & \texttt{.**} +\end{tabular}\label{sugar} + +\subsection{Statements} +Squiggle supports \textit{assignment}. Functions are assigned in the form $f(x) = \langle \textit{Expression} \rangle$ + +\begin{grammar} + ::= \texttt{assgn} \alt \texttt{assgnFn} \end{grammar} +With the following obvious sugars + +\begin{tabular}{ c c } + \texttt{assgn} $\langle var \rangle$ $\langle Expression \rangle$ & $\langle var \rangle = \langle Expression \rangle$ \\ + \texttt{assgnFn} $\langle var \rangle$ $\langle var \rangle$ $\langle Expression \rangle$ & $\langle var \rangle (\langle var \rangle) = \langle Expression \rangle$ +\end{tabular} \end{document}