Compare commits

...

7 Commits

Author SHA1 Message Date
Quinn Dougherty
2b5ffb0d2e functions with sugars, base types 2022-03-30 12:00:47 -04:00
Quinn Dougherty
86b9130cbf factor and expression (order of operations) 2022-03-30 06:11:57 -04:00
Quinn Dougherty
f8aa2b0bc2 Expressions (without order of operations) 2022-03-28 19:51:14 -04:00
Quinn Dougherty
da80f1da30 spec/syntax/src: renamed directories 2022-03-28 14:13:07 -04:00
Quinn Dougherty
7933b2632c second commit of spec 2022-03-25 17:08:13 -04:00
Quinn Dougherty
b1887064a7 syntax/result dir gitignored 2022-03-25 15:02:07 -04:00
Quinn Dougherty
1a77a1fac5 syntax init commit 2022-03-25 13:50:40 -04:00
10 changed files with 285 additions and 1 deletions

2
.gitignore vendored
View File

@ -4,3 +4,5 @@ yarn-error.log
.merlin .merlin
.parcel-cache .parcel-cache
.DS_Store .DS_Store
.auctex-auto
result

View File

@ -20,7 +20,7 @@ The playground depends on the components library which then depends on the langu
# Develop # Develop
For any project in the repo, begin by running `yarn` in the top level (TODO: is this true?) For any project in the repo (`packages/*`), begin by running `yarn` in the top level.
``` sh ``` sh
yarn yarn
@ -39,5 +39,16 @@ codium
The `nix develop` shell also provides `yarn`. The `nix develop` shell also provides `yarn`.
# Alpha syntax specification
You can render a pdf of the syntax specification.
``` sh
cd syntax
nix-build
o result/squiggle-spec.pdf
```
Where `o` is `open` if you're on OSX and `xdg-open` if you're on linux.
# Contributing # Contributing
See `CONTRIBUTING.md`. See `CONTRIBUTING.md`.

9
spec/README.md Normal file
View File

@ -0,0 +1,9 @@
# The syntax and semantics of squiggle
We give the syntax in a BNF-like specification
## Render
``` sh
nix-build
```
Shall dump `squiggle-spec.pdf` in the `result` directory.

30
spec/default.nix Normal file
View File

@ -0,0 +1,30 @@
{ chan ? "a7ecde854aee5c4c7cd6177f54a99d2c1ff28a31" # 21.11 tag
, pkgs ? import (builtins.fetchTarball { url = "https://github.com/NixOS/nixpkgs/archive/${chan}.tar.gz"; }) {}
}:
# Style sheets https://github.com/citation-style-language/styles/
with pkgs;
let deps = [
(texlive.combine
{ inherit (texlive)
scheme-full;
}
)
];
in
stdenv.mkDerivation {
name = "render_squiggle-spec";
src = ./src;
buildInputs = deps;
buildPhase = ''
echo rendering...
pdflatex main
biber main
pdflatex main
pdflatex main
echo rendered.
'';
installPhase = ''
mkdir -p $out
cp main.pdf $out/squiggle-spec.pdf
'';
}

5
spec/src/appendix.tex Normal file
View File

@ -0,0 +1,5 @@
\documentclass[../main.tex]{subfiles}
\begin{document}
\section{Appendix}
\end{document}

29
spec/src/biblio.bib Normal file
View File

@ -0,0 +1,29 @@
@book{@PFPL,
author = {Robert Harper},
title = {Practical Foundations for Programming Languages},
year = {2016}
}
@article{@SqgCodePlan,
author = {Ozzie Gooen},
title = {Squiggle Alpha 0.1 Code Plan},
year = {2022},
url = {https://docs.google.com/document/d/1oKTxolRrs-0g0TGEvqCMdhY2FdIjcDj678WUk1iMpx8/edit?usp=sharing}
}
@book{@CraftingInterpreters,
author = {Robert Nystrom},
title = {Crafting Interpreters},
year = {2021},
url = {https://craftinginterpreters.com/contents.html}
}
@article{@SqgSequence,
author = {Ozzie Gooen and Nuno Sempere},
title = {Squiggle (Sequence)},
year = {2020},
url = {https://www.lesswrong.com/s/rDe8QE5NvXcZYzgZ3}
}
@article{@BNFWiki,
author = {Foundation Wikimedia},
year = {2022},
title = {Backus-Naur Form},
url = {https://en.wikipedia.org/wiki/Backus-Naur_form}
}

21
spec/src/introduction.tex Normal file
View File

@ -0,0 +1,21 @@
\documentclass[../main.tex]{subfiles}
\begin{document}
\section{Squiggle: the current document}
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}.
\subsection{Design goals}
We would like, as a programming language, a \textbf{specification} for \textit{expressing beliefs}.
One key difference between this vision and probabilistic programming languages (PPLs) is that for us, the ingest of data is not a factor. See discussion with John Wentworth in \cite{@SqgSequence} for background on the PPL comparison.
\textbf{TODO}
\end{document}

30
spec/src/main.tex Normal file
View File

@ -0,0 +1,30 @@
\documentclass{article}
\usepackage[utf8]{inputenc}
\usepackage{syntax}
\setlength{\grammarparsep}{2ex plus 0.1ex minus 0.05ex}
% \usepackage[T1]{fontenc}
% \usepackage{bussproofs}
\usepackage{amsfonts}
\usepackage{subfiles}
\usepackage{datetime}
\usepackage{hyperref}
\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 - \texttt{quinn@quantifieduncertainty.org}}
\date{This render: \today}
\begin{document}
\maketitle{}
\nocite{*}
\subfile{introduction}
\subfile{syntax}
\subfile{semantics}
\subfile{appendix}
\printbibliography
\end{document}

7
spec/src/semantics.tex Normal file
View File

@ -0,0 +1,7 @@
\documentclass[../main.tex]{subfiles}
\begin{document}
\section{Semantics}\label{section:semantics}
\textbf{TODO: Operational semantics}.
\end{document}

140
spec/src/syntax.tex Normal file
View File

@ -0,0 +1,140 @@
\documentclass[../main.tex]{subfiles}
\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
\begin{grammar}
<type> ::= <GenericDist> \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}
<GenericDist> ::= <PointSetDist> \alt \texttt{SampleSet} \alt <Symbolic>
<PointSetDist> ::= \texttt{Mixed} \alt \texttt{Continuous} \alt \texttt{Discrete}
<Symbolic> ::= \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}\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$, though this story is suppresses a lot of the detail that would make opertational semantics possible.
\begin{grammar}
<Factor> ::= <GenericDist> \alt \texttt{float} \alt list(<type>) \alt <var> \alt <Factor> * <Factor> \alt <Factor> .* <Factor> \alt <Factor> ./ <Factor>
<Expression> ::= <Factor> \alt <Factor> + <Factor> \alt <Factor> .+ <Factor> \alt <Factor> - <Factor> \alt <Factor> .- <Factor>
\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}
<GenericDist> ::= <GenericDist> \alt \texttt{normalize}\ <NonNormalizedDist>
<NonNormalizedDist> ::=
<GenericDist>
\alt \texttt{distFloatAdd} <NonNormalizedDist> \texttt{float}
\alt \texttt{distFloatMultiply} <NonNormalizedDist> \texttt{float}
\alt \texttt{distFloatSubtract} <NonNormalizedDist> \texttt{float}
\alt \texttt{distFloatDivide} <NonNormalizedDist> \texttt{float}
\alt \texttt{distFloatExponent} <NonNormalizedDist> \texttt{float}
\alt \texttt{pointwiseAddConstant} <NonNormalizedDist> \texttt{float}
\alt \texttt{pointwiseMultiplyConstant} <NonNormalizedDist> \texttt{float}
\alt \texttt{pointwiseSubtractConstant} <NonNormalizedDist> \texttt{float}
\alt \texttt{pointwiseDivideConstant} <NonNormalizedDist> \texttt{float}
\alt \texttt{pointwiseLogConstant} <NonNormalizedDist> \texttt{float}
\alt \texttt{distDistAdd} <NonNormalizedDist> <NonNormalizedDist>
\alt \texttt{distDistSum} list(<NonNormalizedDist>)
\alt \texttt{distDistMultiply} <NonNormalizedDist> <NonNormalizedDist>
\alt \texttt{distDistProduct} list(<NonNormalizedDist>)
\alt \texttt{distDistSubtract} <NonNormalizedDist> <NonNormalizedDist>
\alt \texttt{distDistDivide} <NonNormalizedDist> <NonNormalizedDist>
\alt \texttt{distDistExponent} <NonNormalizedDist> <NonNormalizedDist>
\alt \texttt{pointwiseDistAdd} <NonNormalizedDist> <NonNormalizedDist>
\alt \texttt{pointwiseDistSum} list(<NonNormalizedDist>)
\alt \texttt{pointwiseDistMultiply} <NonNormalizedDist> <NonNormalizedDist>
\alt \texttt{pointwiseDistProduct} list(<NonNormalizedDist>)
\alt \texttt{pointwiseDistSubtract} <NonNormalizedDist> <NonNormalizedDist>
\alt \texttt{pointwiseDistDivide} <NonNormalizedDist> <NonNormalizedDist>
\alt \texttt{pointwiseDistExponent} <NonNormalizedDist> <NonNormalizedDist>
\alt \texttt{truncate} <NonNormalizedDist> \texttt{float} \texttt{float}
\alt \texttt{truncateLeft} <NonNormalizedDist> \texttt{float}
\alt \texttt{truncateRight} <NonNormalizedDist> \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}
<float> ::=
\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} <GenericDist> \texttt{float}
\alt \texttt{invPdfPoint} <GenericDist> \texttt{float}
\alt \texttt{cdfPoint} <GenericDist> \texttt{float}
\alt \texttt{mean} <GenericDist>
\alt \texttt{sample} <GenericDist>
\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}
<statement> ::= \texttt{assgn} <var> <Expression> \alt \texttt{assgnFn} <var> <var> <Expression>
\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}