λ-Prolog

Term = abs(\f->abs(\x->app f(app f x))), has_type Term Type.

This is an interpreter for a dialect of the programming language λ-Prolog.

Usage:

• End every query with a period.
• Write everything in lower-case except for query variables.
• Write function application and abstraction just like in Haskell, e. g. \ x -> x or f x y.
• You can use the two built-in constants: all and the infix operator ==>.
• You can write % x -> f x instead of all (\ x -> f x).
• Use add_rule to add a rule.
• Type more. to see if there are more solutions to the query you entered.

Example:

Copy the example queries into the input field one by one.

• Rules for appending lists:
  add_rule (%xs-> append nil xs xs).
add_rule (%x xs ys zs->append xs ys zs==>append (cons x xs) ys (cons x zs)).
• A query:
  append Xs Ys (cons 0 (cons 1 nil)).