employer
/
tame
1
0
Fork 0
Code Packages Releases Activity
tame/design/tpl/tpl.sty

129 lines
3.6 KiB
Plaintext
Raw Normal View History

design/tpl: The Tame Programming Language initial concept There's a lot of change that's likely going to take place with this thing, but it's a start. The abstract summarizes the purpose of this---to formally define TAME in terms of algebra, first-order logic, and [ZFC] set theory. This came about while working on compiler changes and optimizations, since it's difficult to ensure correctness (and discover further optimizations) without being able to formally define the language. The focus at the moment is the classification system rewrite, which can be expressed in terms of first order logic and set theory. This commit contains essentially a POC with some carefully chosen mathematical foundations (abstractions of which are subject to change) and a basic representation of a subset of the classification system for scalars.
2021-04-30 09:16:01 -04:00
% The TAME Programming Language glossary
%
% Copyright (C) 2021 Ryan Specialty Group, LLC.
%
% Licensed under the Creative Commons Attribution-ShareAlike 4.0
% International License.
%%
% Concrete Mathematics fonts
\usepackage[amsfonts,amssymb]{concmath}
\usepackage{makeidx}
% Note that we force draft=false so hyperlinks always appear
\usepackage[colorlinks=true,linkcolor=href,draft=false]{hyperref}
design/tpl: Show listings in draft mode What an odd default.
2021-05-11 13:08:25 -04:00
% For displaying source code (e.g. XML); `final' needed in draft mode,
% otherwise no listings display.
\usepackage[final]{listings}
design/tpl: The Tame Programming Language initial concept There's a lot of change that's likely going to take place with this thing, but it's a start. The abstract summarizes the purpose of this---to formally define TAME in terms of algebra, first-order logic, and [ZFC] set theory. This came about while working on compiler changes and optimizations, since it's difficult to ensure correctness (and discover further optimizations) without being able to formally define the language. The focus at the moment is the classification system rewrite, which can be expressed in terms of first order logic and set theory. This commit contains essentially a POC with some carefully chosen mathematical foundations (abstractions of which are subject to change) and a basic representation of a subset of the classification system for scalars.
2021-04-30 09:16:01 -04:00
% Definitions, theorems, proofs, etc
design/tpl: Remove glossary This is an unnecessary feature to maintain right now. I will include symbols at the very beginning of the index, which is common in mathematics texts, and may will add a table of common symbols in the future.
2021-05-10 14:28:37 -04:00
\usepackage{amsmath}
design/tpl: The Tame Programming Language initial concept There's a lot of change that's likely going to take place with this thing, but it's a start. The abstract summarizes the purpose of this---to formally define TAME in terms of algebra, first-order logic, and [ZFC] set theory. This came about while working on compiler changes and optimizations, since it's difficult to ensure correctness (and discover further optimizations) without being able to formally define the language. The focus at the moment is the classification system rewrite, which can be expressed in terms of first order logic and set theory. This commit contains essentially a POC with some carefully chosen mathematical foundations (abstractions of which are subject to change) and a basic representation of a subset of the classification system for scalars.
2021-04-30 09:16:01 -04:00
\usepackage{amsthm}
% Line spacing instead of indentation for paragraphs
%\usepackage[parfill]{parskip}
\usepackage{xcolor}
% To aid in defining star commands
\usepackage{suffix}
% Colors from Tango Icon Theme
% https://en.wikipedia.org/wiki/Tango_Desktop_Project
\definecolor{href}{HTML}{204a87}
% TAME is typeset in smallcaps
\newcommand{\tame}{\textsc{Tame}}
design/tpl: TAMER case fix 'T' was lowercased.
2021-05-11 11:32:14 -04:00
\newcommand{\tamer}{\textsc{Tamer}}
design/tpl: The Tame Programming Language initial concept There's a lot of change that's likely going to take place with this thing, but it's a start. The abstract summarizes the purpose of this---to formally define TAME in terms of algebra, first-order logic, and [ZFC] set theory. This came about while working on compiler changes and optimizations, since it's difficult to ensure correctness (and discover further optimizations) without being able to formally define the language. The focus at the moment is the classification system rewrite, which can be expressed in terms of first order logic and set theory. This commit contains essentially a POC with some carefully chosen mathematical foundations (abstractions of which are subject to change) and a basic representation of a subset of the classification system for scalars.
2021-04-30 09:16:01 -04:00
% TODO: highlighting
\lstset{
language=XML,
basicstyle=\ttfamily,
columns=fullflexible,
keepspaces=true,
showstringspaces=false,
}
\newcommand\xpath[1]{\texttt{#1}}
\newcommand\xmlnode[1]{\texttt{#1}}
\newcommand\xmlattr[1]{@\texttt{#1}}
\newcommand\tameparam[1]{\texttt{#1}}
\newcommand\tameclass[1]{\texttt{#1}}
\newcommand\tameconst[1]{\texttt{#1}}
\newcommand\true{\ensuremath{\top}}
\newcommand\false{\ensuremath{\bot}}
\newcommand\Bool{\ensuremath{\{\false,\true\}}}
\newcommand\logand{\ensuremath{\wedge}}
\newcommand\logor{\ensuremath{\vee}}
\newcommand\tametrue{\tameconst{TRUE}}
\newcommand\tamefalse{\tameconst{FALSE}}
\newcommand\Int{\ensuremath{\mathbb{Z}}}
\newcommand\Real{\ensuremath{\mathbb{R}}}
\newcommand\Set[1]{\ensuremath{\left\{#1\right\}}}
\newcommand\Fam[3]{\ensuremath{\left\{#1_{#2}\right\}_{#2\in #3}}}
\newcommand\Vectors{\ensuremath{\mathcal{V}}}
\newcommand\Vector[1]{\ensuremath{\left\langle#1\right\rangle}}
\newcommand\VFam[3]{\ensuremath{\Vector{#1_{#2}}_{#2\in #3}}}
\newcommand\Matrices{\ensuremath{\Vectors^{\Vectors^\Real}}}
\let\union\cup
design/tpl: Mostly-complex symbol index entries for Chapter 0
2021-05-11 11:33:12 -04:00
\let\intersect\cap
design/tpl: \vdash=>\infer and index entry
2021-05-10 16:54:19 -04:00
\let\infer\vdash
design/tpl: The Tame Programming Language initial concept There's a lot of change that's likely going to take place with this thing, but it's a start. The abstract summarizes the purpose of this---to formally define TAME in terms of algebra, first-order logic, and [ZFC] set theory. This came about while working on compiler changes and optimizations, since it's difficult to ensure correctness (and discover further optimizations) without being able to formally define the language. The focus at the moment is the classification system rewrite, which can be expressed in terms of first order logic and set theory. This commit contains essentially a POC with some carefully chosen mathematical foundations (abstractions of which are subject to change) and a basic representation of a subset of the classification system for scalars.
2021-04-30 09:16:01 -04:00
\newcommand\len[1]{\ensuremath{\left|#1\right|}}
\numberwithin{equation}{section}
% Allows us to switch between styles, if need be
% (e.g. I used the colon style before adopting notation from type theory
% where the colon became ambiguous)
\newcommand\Forall{\@ifstar\@Forallstar\@Forall}
\newcommand\@Forall[2]{\forall #1\left(#2\right)}
\newcommand\@Forallstar[2]{\forall #1 #2}
\newcommand\Exists{\@ifstar\@Existsstar\@Exists}
\newcommand\@Exists[2]{\exists #1\left(#2\right)}
% Without \left and \right. You'll also need this if you use `&' in an
% `align' environment within an argument.
\newcommand\@Existsstar[2]{\exists #1 #2}
\theoremstyle{definition}
\newtheorem{definition}{Definition}[section]
\newcommand\dfnlabel[1]{\label{dfn:#1}}
\newcommand\dfnref[1]{Definition~\ref{dfn:#1}}
\newcommand\dfnpref[1]{Definition~\pref{dfn:#1}}
\theoremstyle{plain}
\newtheorem{corollary}{Corollary}[section]
\newcommand\corlabel[1]{\label{cor:#1}}
\newcommand\corref[1]{Corollary~\ref{cor:#1}}
\newcommand\corpref[1]{Corollary~\pref{cor:#1}}
\theoremstyle{remark}
\newtheorem{remark}{Remark}[section]
\newcommand\pref[1]{\ref{#1} on page~\pageref{#1}}
\newcommand\seclabel[1]{\label{sec:#1}}
\newcommand\secref[1]{Section~\ref{sec:#1}}
\newcommand\secpref[1]{Section~\pref{sec:#1}}
% Binary function composition
design/tpl: bicomp: Use superscript instead of stacking Stacking originally seemed like a good idea, but perhaps this does read a bit better (and looks more like the composition operation being applied), and composes a bit better if we needed e.g. \bicomp\bicomp{R}. It's also less ambiguous when it's over a larger expression. For example, \bicomp{[A]} places \circ over top of the A, which looks as if it's [\bicomp{A}]. It's obvious what the intention is in that context, since \bicomp{A} makes no sense, but there could be other situations where it doesn't. With this change, it results in {[A]}^\circ.
2021-05-10 14:11:16 -04:00
\newcommand\bicomp[1]{{#1}^\circ}
\newcommand\bicompi[1]{{#1}^\bullet}
design/tpl: The Tame Programming Language initial concept There's a lot of change that's likely going to take place with this thing, but it's a start. The abstract summarizes the purpose of this---to formally define TAME in terms of algebra, first-order logic, and [ZFC] set theory. This came about while working on compiler changes and optimizations, since it's difficult to ensure correctness (and discover further optimizations) without being able to formally define the language. The focus at the moment is the classification system rewrite, which can be expressed in terms of first order logic and set theory. This commit contains essentially a POC with some carefully chosen mathematical foundations (abstractions of which are subject to change) and a basic representation of a subset of the classification system for scalars.
2021-04-30 09:16:01 -04:00
\let\xml\texttt
design/tpl: Begin symbol list at beginning of index
2021-05-10 16:50:30 -04:00
% Symbols appear at the beginning of the index
\newcommand\indexsym[2]{\index{__sym_#2@{\ensuremath{#1}}|see {#2}}}