H. Hernan Moraldo - personal archive
home about faq contact website

HQL - HHM's Quantified Lambda

Dated: miércoles, julio 13, 2005

HQL stands for HHM's Quantified Lambda (or Hernan's Quantified Lambda), and is a small functional language, whose expressions can involve the use of quantifier operators (for all, exists, etc).

It surely isn't a brilliant masterpiece, but it was a fun thing to do back then (july 2004), and even now it's surely interesting to see.



Downloads:







Full paper in HTML:
(see above for pdf and latex version)

HQL's language specification

by H. Hernán Moraldo

http://www.hhm.com.ar/ June 2005



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



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).

To make this program a real HQL program, all have to be converted to form, and binary operators like , and 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:

Where code like is applying the function contained in variable to the expression .

The same program is presented in Haskell syntax as follows:

 xTerm6=(tForAllB "x"
  (tForAllB "y"
  (tIif 
  (tOr (tNot (TVar "x")) (TVar "y"))
  (tLogicIf (TVar "x") (TVar "y"))
  )
  )
  )

Where functions like and 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 . The program semantics is in this case , as the program is describing a truth that does not depend on any external variables (excepting those of the library).



HQL's language specification



Type inference



Definitions:



Base:



Integers:



Booleans:



Application:



Lambda:



Let .. in:



Explicit let .. in



If .. then .. else:



Exists:

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



Not:



IIIOp (others operators are similar):



Semantics



Environments:

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



Big K definition:



Integer constants:



Boolean constants:



Variables:



Lambdas:



Let .. in:



App:



If .. then .. else:



Not:



Exists in booleans:



Exists in Range of Integers:



IIIOp:



Bibliography



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



About this document ...



HQL's language specification

This document was generated using the LaTeX2HTML translator Version 2002-2-1 (1.71)



In categories: All Articles English Mathematics 2004 2005




Copyright 2000-2008 by Horacio Hernán Moraldo
All rights reserved