% This module illustrates the encoding of Hilbert's Tenth Problem into
% the problem of determining if flexible-flexible disagreement pairs
% have *closed* solutions when not all types are know to be empty.
% For the correctness proof of this encoding, see
%
% D. Miller, ``Unification under a mixed prefix'', Journal of
% Symbolic Computation, volume 14, 321-358 (1992).
%
% The reduction used here is similar to the one found in
%
% W. Goldfarb, ``The Undecidability of the Second-Order
% Unification Problem,'' Theoretical Computer Science 13, 1981,
% 225 -- 230.
%
% Notice that lambda Prolog cannot be used to actually solve the
% encoded problems since all the computation gets done in
% flexible-flexible pairs, which are not processed much in lambda Prolog.
% This file is useful in only showing the reduction to flex-flex
% pairs.
module hilbert.
kind i type.
% Notice that there are no constructors for objects in type i. This
% allows you to conclude that the only closed terms of
% (i -> i) -> (i -> i)
% are the Church numerals.
type zero, one, church ((i -> i) -> (i -> i)) -> o.
type plus, mult
(((i -> i) -> i -> i) -> ((i -> i) -> i -> i) ->
((i -> i) -> i -> i)) -> o.
type succ (((i -> i) -> i -> i) -> ((i -> i) -> i -> i)) -> o.
type problem1 ((i -> i) -> i -> i) -> ((i -> i) -> i -> i) ->
((i -> i) -> i -> i) -> ((i -> i) -> i -> i) -> o.
% Three combinators for Church arithmetic. succ is not needed given
% plus, but it's convenient.
succ (N\F\X\ (N F (F X))).
plus (N\M\F\X\ ((N F) (M F X))).
mult (N\M\F\X\ (N (M F) X)).
% The definitions for Church numerals below are not used in the
% encoding. They are included just for convenience. They are not used
% since they contribute flexible-rigid pairs: only flexible-flexible
% pairs are wanted.
church (F\X\ X).
church (F\X\ (C F (F X))) :- church C.
% Here is how to describe zero and one using flexible-flexible pairs.
% zero is the only solution to the equation
% z = z + z
zero Z :- plus P, Z = (P Z Z).
% one is the only solution to the equation
% z + z = z + 1
one O :- plus P, succ S, (P O O) = (S O).
% Now, encode the following set of equations:
% { x = 1, u = x + x, x + y = z, y * z = u }
% This set has exactly one solution: x = 1, u = 2, y = 1, z = 2.
problem1 X U Y Z :-
one O, plus P, mult M,
X = O, U = (P X X), Z = (P X Y), U = (M Y Z).
% ?- zero Z.
%
% Z = Z
%
% The remaining flexible - flexible pairs:
% .
% yes
% ?- one Z.
%
% Z = Z
%
% The remaining flexible - flexible pairs:
% .
% yes
% This is the result of problem 1 using LP2.6. If only closed terms are
% allowed for Var1 and Var6, then both of these must be the Church
% numeral 1 to satisfy the flexible-flexible pairs below. The bound
% variables names were changed to make this example more readable.
%
% ?- problem1 U V W Y.
%
% U = Var1,
% V = F \ X \ (Var1 F (Var1 F X)),
% W = Var6,
% Y = F \ X \ (Var1 F (Var6 F X))
%
% The remaining flexible - flexible pairs:
%
% .
% Notice that using the predicate church, we can attempt to solve these
% equational systems using a naive generate and test stradegy. In the
% following example, the flexible-flexible pairs for constraints which
% are tested against successive integers.
%
% ?- problem1 X U Y Z, church U.
%
% X = F \ X \ (F X)
% Y = F \ X \ (F X)
% Z = F \ X \ (F (F X))
% U = F \ X \ (F (F X))
%
% This is a pretty silly way to solve such equations in practice.