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

Lectures / Modules / Homeworks / Syllabus