\documentclass[a4paper,12pt]{article}
\begin{document}

\title{HQL's language specification}
\author{H. Hern\'{a}n Moraldo\\http://www.hhm.com.ar/\\mg@moraldo.com.ar}
\date{June 2005}
\maketitle





\section{About HQL}

HQL stands for `HHM's Quantified Lambda' and it's a small programming language I created in 2004, for an Advanced Functional Programming class I had with professor Pablo E. Martinez Lopez. It's a very simple functional language, whose expressions can involve the use of quantifier operators (for all, exists, etc).

The following document presents the language formal specification, that is, the type inference for the language, and its semantics. It's the copy of the original hand-written specification, so it might be incomplete.

Visit http://www.hhm.com.ar/ to download the interpreter (with no parser) source code, and for any questions and comments, send mail to mg@moraldo.com.ar

\section{A sample program}

We want to have an example of the use of HQL, that shows what kind of language it is, and what kind of programs can be written with it.

Next code, shows a program written in HQL's abstract syntax (as there is no parser yet, you might have to convert it to Haskell data before executing it with the interpreter).

\[
\begin{array}{c}
program =
\forall x \in \left.Bool\right. . \left(
	\forall y \in \left.Bool\right. . \left(
		\left(
			\neg
			\left(
				x \vee y
			\right)
		\right)
	\leftrightarrow
		\left(
			x \rightarrow y
		\right)
	\right)
\right)
\end{array}
\]

To make this program a real HQL program, all $\forall$ have to be converted to $\exists$ form, and binary operators like $\leftrightarrow$, $\vee$ and $\neg$ have to be converted either to BBBOp form, or to applications of functions as defined in the library (library is a non empty initial environment, as the one used by the interpreter). The full converted program would be:

\[
\begin{array}{c}
program =
\forall x \in \left.Bool\right. .
	\forall y \in \left.Bool\right. . 
\\
	\left.app\right.
	\left(
	\left.app\right. iif
		\left(
			\left.app\right. not
			\left(
				\left.app\right.
					\left(\left.app\right. or \left.x\right.\right)
				y
			\right)
		\right)
	\right)
		\left(
			\left.app\right.
				\left(\left.app\right. if \left.x\right.\right)
			y
		\right)
\end{array}
\]

Where code like $\left.app\right. or x$ is applying the function contained in variable $or$ to the expression $x$.

The same program is presented in Haskell syntax as follows:

\begin{verbatim}
xTerm6=(tForAllB "x"
           (tForAllB "y"
             (tIif 
               (tOr (tNot (TVar "x")) (TVar "y"))
               (tLogicIf (TVar "x") (TVar "y"))
             )
           )
       )
\end{verbatim}

Where functions like $tForAllB$ and $tIif$ have been previously defined to make programming much faster.

It's interesting to ask what type has this program. According to the type inference algorithm, it's a $Bool$. The program semantics is in this case $\underline{True}$, as the program is describing a truth that does not depend on any external variables (excepting those of the library).

\section{HQL's language specification}

\subsection{Type inference}

\subsubsection{Definitions:}

\[ Type = \left.Bool\right. | \left.Int\right. | \left.Type \rightarrow Type\right. \]

\[
\begin{array}{c}
e :=
\left.v\right. |
\left.c_i\right. |
\left.c_b\right. |
\left.app\right. \left.e\right. \left.e\right. |
\left.lam\right. \left.t\right. \left.v\right. \left.e\right. | \\
\left.let\right. v=e \left.in\right. e |
\left.explicitLet\right. v=e \in e \left.in\right. e | \\
\exists v \in t . e |
\neg e |
\left.if\right. \left.e\right. \left.e\right. \left.e\right. 
\end{array}
\]

\subsubsection{Base:}

\[ \frac {v:s \in \Gamma} { \Gamma \vdash v:s } \]

\subsubsection{Integers:}

\[ \frac {} { \Gamma \vdash c_i:Int } \]

\subsubsection{Booleans:}

\[ \frac {} { \Gamma \vdash c_b:Bool } \]

\subsubsection{Application:}

\[ \frac
{ \Gamma\vdash e_1:t_1\rightarrow t_2  \hspace{1cm}  \Gamma\vdash e_2:t_1 }
{ \Gamma\vdash \left.app\right. \left.e_1\right. \left.e_2\right.:t_2 }
\]

\subsubsection{Lambda:}

\[ \frac
{ \Gamma _{v,} v:t_1 \vdash e:t_2 }
{ \Gamma\vdash \left.lam\right. v\in t_1 . e: t_1 \rightarrow t_2 }
\]

\subsubsection{Let .. in:}

\[ \frac
{
\begin{array}{c}
\Gamma \vdash e_1:t_1 \\
\Gamma _{v,} v:t_1 \vdash e_2:t_2
\end{array}
}
{ \Gamma\vdash \left.let\right. v=e_1 \left.in\right. e_2:t_2 }
\]

\subsubsection{Explicit let .. in}

\[ \frac
{
\begin{array}{c}
\Gamma \vdash e_1:t \\
\Gamma _{v,} v:t \vdash e_2:t_2
\end{array}
}
{ \Gamma\vdash \left.explicitLet\right. v=e_1 \in t \left.in\right. e_2:t_2 }
\]

\subsubsection{If .. then .. else:}

\[ \frac
{ \Gamma\vdash e_1:Bool  \hspace{1cm}  \Gamma\vdash e_2:t \hspace{1cm}  \Gamma\vdash e_3:t}
{ \Gamma\vdash \left.ifthenelse\right. \left.e_1\right. \left.e_2\right. \left.e_3\right. : t }
\]

\subsubsection{Exists:}

\[ \frac
{ \Gamma _{v,} v:ht \vdash e:Bool }
{ \Gamma\vdash \exists v \in t. e : Bool }
\]

$h$ would require some extra detail to be thrown in this specification. For now, let's just say that the $t$ in $\exists v \in t. e$ is a special type, that can be bool or a restricted integer, so $h$ is a function that converts these special types into the ones accepted by the system.

\subsubsection{Not:}

\[ \frac
{ \Gamma \vdash e:Bool }
{ \Gamma\vdash \left.not\right. e : Bool }
\]

\subsubsection{IIIOp (others operators are similar):}

\[ \frac
{ \Gamma\vdash e_1:Int  \hspace{1cm}  \Gamma\vdash e_2:Int }
{ \Gamma\vdash \left.IIIOp\right. \left.s\right. \left.e_1\right. \left.e_2\right. : Int  }
\]


\subsection{Semantics}

\subsubsection{Environments:}

Environments are sets of triples like this: $ \left( \beta, v, t \right) $ , with $v$ being a variable name, $t$ the expression associated to $v$ (its value), and $\beta$ the environment where $v$ is defined.


\subsubsection{Big K definition:}

\[
\mathbf{K}\left(\alpha, v, e\right)=\left( \alpha+\mathbf{K}\left(\alpha, v, e\right), v, e \right)
\]

\subsubsection{Integer constants:}

\[
\left[\left[ c_i \right]\right] _\alpha := \underline{c_i}
\]

\subsubsection{Boolean constants:}

\[
\left[\left[ c_b \right]\right] _\alpha := \underline{c_b}
\]

\subsubsection{Variables:}

\[
\left[\left[ v \right]\right] _\alpha :=
\left[\left[ t \right]\right] _\beta \mbox{, if } \left(\beta, v, t\right)\in \alpha
\]

\subsubsection{Lambdas:}

\[
\left[\left[ \left.lam\right. v \in s . e \right]\right] _\alpha :=
\left.\underline{lam}\right. \left.v\right. \left.e\right. \alpha
\]

\subsubsection{Let .. in:}

\[
\left[\left[ \left.let\right. \left.v\right. \left.e_1\right. e_2 \right]\right] _\alpha :=
\left[\left[e_2\right]\right]
_{\alpha + \mathbf{K} \left( \alpha, v, e_1 \right)}
\]


\subsubsection{App:}

\[
\left[\left[ \left.app\right. \left.e_1\right. e_2 \right]\right] _\alpha :=
\left[\left[e_3\right]\right]
_{\beta + \mathbf{K} \left( \alpha, v, e_2 \right)}
\mbox{ if }
\left[\left[e_1\right]\right]_\alpha=
\left.\underline{lam}\right. \left.v\right. \left.e_3\right. \beta
\]

\subsubsection{If .. then .. else:}

\[
\left[\left[ \left.ifthenelse\right. \left.e_1\right. \left.e_2\right. e_3 \right]\right]_\alpha:=
\left\lbrace
\begin{array}{c}
\left[\left[e_2\right]\right]_\alpha
\mbox{, if } \left[\left[e_1\right]\right]_\alpha=\underline{true}
\vspace{0.5cm}
\\
\left[\left[e_3\right]\right]_\alpha
\mbox{, otherwise }
\end{array}
\right.
\]

\subsubsection{Not:}

\[
\left[\left[ \left.not\right. e \right]\right]_\alpha:=
\neg \left[\left[ e \right]\right]_\alpha
\]

\subsubsection{Exists in booleans:}

\[
\left[\left[ \exists v \in Bool .e \right]\right] _\alpha :=
\left[\left[e\right]\right]
_{\alpha + \left( \alpha, v, True \right)}
\vee
\left[\left[e\right]\right]
_{\alpha + \left( \alpha, v, False \right)}
\]

\subsubsection{Exists in Range of Integers:}

\[
\left[\left[ \exists v \in [i_1 .. i_2] .e \right]\right] _\alpha :=
\left\lbrace
\begin{array}{c}
\left[\left[e\right]\right]
_{\alpha + \left( \alpha, v, i_1 \right)}
\vee
\left[\left[ \exists v \in [i_1 + 1 .. i_2] .e \right]\right] _\alpha
\mbox{, if } e_1 \leq e_2
\vspace{0.5cm}
\\
\underline{False}
\mbox{, otherwise }
\end{array}
\right.
\]


\subsubsection{IIIOp:}

\[
\left[\left[ \left.IIIOp\right. \left.id\right. \left.n_1\right. n_2 \right]\right] _\alpha :=
\left\lbrace
\begin{array}{c}
\left[\left[ n_1 \right]\right] _\alpha + \left[\left[ n_2 \right]\right] _\alpha
\mbox{, if } id = \mbox{'$+$'}
\vspace{0.5cm}
\\
\left[\left[ n_1 \right]\right] _\alpha * \left[\left[ n_2 \right]\right] _\alpha
\mbox{, if } id = \mbox{'$*$'}
\vspace{0.5cm}
\\
\mbox{et cetera}
\end{array}
\right.
\]



\section{Bibliography}

Reynolds, J. C. (1998). \emph{Theories of Programming Languages.} Cambridge University Press. New York.



\end{document}
