A Haskell Nominal Toolkit

Haskell Nominal ToolKit(HNT) is composed of an Haskell library providing:

• alpha-equivalence, matching and rewriting algorithms with freshness contexts
• a monadic framework handling environments, freshness contexts, substitutions easily
• a generic zipper implementation

and an interactive rewriting tool providing rewriting/updating on any subterm.

The interactive tool has to be seen as a tech-demo of the library possibilities.

1  Links

• Darcs repository
• Documentation
• Download page

2  Downloading

• via darcs: type in a shell: darcs get http://perso.crans.org/calves/hnt/hnt-darcs
• via the Download page

3  Installation

To install HNT, GHC is required. The package uses cabal, you can build and install it in the usual cabal way. Run in a shell:

cd <package directory>
runhaskell Setup.lhs configure
runhaskell Setup.lhs build
runhaskell Setup.lhs install

4  Interactive tool tutorial

The interactive tool executable is named hnt. Is has to be run in a shell.

4.1  Syntax

In the following, X represents an Integer, t, s and u three terms.

4.1.1  Terms

A term is either:

• a:X is an atom
• c:X is a constant
• v:X is a variable
• (a:X a:X) t is a swapping
• [a:X] t is an abstraction
• (t , u) is a pair

4.1.2  Freshness Context, Rewriting Rule and Term in Context

• a freshness context fc is {a:X ... a:X}#v:X ... {a:X .... a:X}#v:X
• a rewriting rule rl is fc |- t -> s
• a term in context tc is fc |- t

4.2  Commands

• help: print an help message
• move down: move to the first subterm
• move down to left: move to the left subterm
• move down to right: move to the right subterm
• move down to modal: move to the modal subterm
• move up: move up
• move down: move to the next unvisited position
• update t: replace the current subterm by t
• rewrite rl: apply the rule rl to the current subterm
• context fc: replace the freshness context by fc

This document was translated from L^AT_EX by H^EV^EA.