Below is the signature for a first-order object-logic and some
sample formulas.
% Term constructors
kind term type.
type a term.
type b term.
type f term -> term.
type g term -> term -> term.
% Logical constants
kind form type.
type truth form.
type false form.
type neg form -> form.
type or form -> form -> form.
type and form -> form -> form.
type imp form -> form -> form.
type all (term -> form) -> form.
type some (term -> form) -> form.
% Non-logical constants
type r form.
type p term -> form.
type q term -> term -> form.
type example int -> form -> o.
example 1 (and r (p a)).
example 2 (all x\(and r (p x))).
example 3 (all x\(some y\(imp (q x y) (all y\(q y (g x y)))))).
example 4 (some x\ (all x\(p x))).
Write a predicate count_q to determine the number of
quantifier occurrences that appear in an object-level formula (a term of
type form).
Your code should produce the following answers for the above examples.
?- example N F, count_q F M.
M = 0,
F = and r (p a),
N = 1.
;
M = 1,
F = all [x:term] and r (p x),
N = 2.
;
M = 3,
F = all [x:term] some [y:term] imp (q x y) (all [y1:term] q y1 (g x y1)),
N = 3.
;
M = 2,
F = some [x:term] all [x1:term] p x1,
N = 4.
;
no more solutions
?-
There is a presentation of lambda-terms that does not use bound variables.
Rather, variables are replaced with postive integers that are used to
point backwards to the quantifier in which it is bound. The task for
this problem is to implement a program that converts formulas in the
above syntax (that use explicit bound variables) to formulas in the
following syntax (that use integers as pointers).
% Term constructors
kind term' type.
type a' term'.
type b' term'.
type f' term' -> term'.
type g' term' -> term' -> term'.
% Logical constants
kind form' type.
type truth' form'.
type false' form'.
type neg' form' -> form'.
type or' form' -> form' -> form'.
type and' form' -> form' -> form'.
type imp' form' -> form' -> form'.
type all' form' -> form'.
type some' form' -> form'.
type v int -> term'.
% Non-logical constants
type r' form'.
type p' term' -> form'.
type q' term' -> term' -> form'.
Write a couple of conversion predicates
type convertF form -> form' -> int -> o.
type convertT term -> term' -> int -> o.
to transform terms and formulas in the first syntax to the second (these
predicates probably cannot be reversed since you will need to use the
is predicate to compute on the integer counters. You should be
able to get the following result.
?- example N F, convertF F F' 0.
F' = and' r' (p' a'),
F = and r (p a),
N = 1.
;
F' = all' (and' r' (p' (v 1))),
F = all x\(and r (p x)),
N = 2.
;
F' = all' (some' (imp' (q' (v 2) (v 1)) (all' (q' (v 1) (g' (v 3) (v 1)))))),
F = all x\(some y\(imp (q x y) (all y1\(q y1 (g x y1))))),
N = 3.
;
F' = some' (all' (p' (v 1))),
F = some x\(all x1\(p x1)),
N = 4.
;
no more solutions
?-
This style of lambda-term representation is called nameless dummies
or de Bruijn's representation named after N. de Bruijn who first
presented them in Lambda Calculus Notation with Nameless
Dummies, a Tool for Automatic Formula Manipulation, with Application to
the Church-Rosser Theorem (Indag. Math., 34(5) 1972, 381-392).