# CSE 360 Homework 6

1. 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
?-
```
2. 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).

Lectures / Modules / Homeworks / Syllabus