About language

Nλ is a simple functional programming language aimed at manipulating infinite, but first-order definable structures, such as the countably infinite clique graph or the set of all intervals with rational endpoints. Internally, such sets are represented by logical formulas that define them, and an external satisfiability modulo theories (SMT) solver is regularly run by the interpreter to check their basic properties.

You can read more about the language in an article
SMT Solving for Functional Programming over Infinite Structures.

Get article
Next

Application

The language has been used to implement an algorithm to learn nominal automata - the extension of the original algorithm, by Dana Angluin, to languages over infinite (structured) alphabets. In particular with this algorithm you can learn a subclass of nominal non-deterministic automata.

More information about algorithm you can find in an article
Learning nominal automata (POPL 2017).

Get article
Next

Online console

You can try out the language in your browser with online console. This is Nλ interpreter to evaluate Haskell expressions using NLambda package. It allows switching between two structures of atoms: equality atoms and ordered atoms (see article for details). It also includes a tutorial with simple examples.

The console does not allow defining own functions in any other way than by let... in... statements. For safety reasons, every command also has a time limit. More complex programs should be run on a computer with installed NLambda.

Powered by Mueval and JQuery Terminal Emulator, inspired by Try Haskell.

Go to console
Next

Documentation

Full documentation of NLambda package is generated by Haddock. It describes the basic types (Variable, Formula, Variants, Atom, Set, etc.), type classes (NominalType, Conditional, Contextual) and functions operating on them. It contains also the source code of the package.

See documentation
Next

Download

You can get Nλ library from GitHub repository or download selected version below:

Version 1.1 Optimizations, bug fixes and new features (constant values) for an article Learning nominal automata.
Version 1.0 Nλ language described in the article SMT Solving for Functional Programming over Infinite Structures
Visit repository
Next

Installation guide

  1. There are two ways to get a source code:
    • download and unpack the package file,
    • check out the source code from git:
      $ git clone https://github.com/szynwelski/nlambda.git
  2. The language is implemented in a Haskell and installation of GHC (at least 7.10) is required.
  3. Move into nlambda directory and perform the following commands: 
    runhaskell Setup configure --user -fTOTAL_ORDER
runhaskell Setup build
runhaskell Setup install
    The flag TOTAL_ORDER is required to install the package with ordered atoms (otherwise equality atoms will be used).
  4. You can also use dedicated scripts:
    • $ ./intall-total-order.shfor ordered atoms,
    • $ ./install-equality.shfor equality atoms.
  5. Additionally, you should install the Z3 Theorem Prover and add it to the PATH environment variable.