Generate typable SK-combinator calculus terms of a given size

sk.pl

:- ensure_loaded(library(aggregate)).

% Generate typable SK-combinator calculus terms of a given size.
%
% Based on Paul Tarau's paper A Hiking Trip Through the Orders of Magnitude:
% Deriving Efficient Generators for Closed Simply-Typed Lambda Terms and Normal
% Forms.
%
% The paper:
% https://arxiv.org/pdf/1608.03912.pdf
%
% An application of the algorithm shown here:
% https://github.com/pedrominicz/sugar
%
% I haven't read it yet, but I think Paul Tarau does (among other things) what
% I do here in this paper: `https://arxiv.org/pdf/1910.01775.pdf`.

% The generating function for SK-combinator calculus terms, given the
% combinatorial class defined by `size/2`, is:
%
%           1 - sqrt(1 - 8z)
%    A(z) = ----------------
%                  2z
%
% The radius of convergence of `A(z)` is:
%
%    rho = 0.125
%
% More generally, if there are `n` combinators, the combinatorial class for the
% analogous size function is:
%
%             1 - sqrt(1 - 4nz)
%    A_n(z) = -----------------
%                    2z
%
% The radius of convergence of `A_n(z)` is:
%
%    rho = 1 / 4n
%
% See section 3 of `https://arxiv.org/pdf/1612.07682.pdf`.
size(s, 0).
size(k, 0).
size(a(X, Y), S) :- size(X, S0), size(Y, S1), S is S0 + S1 + 1.

n2s(0, z) :- !.
n2s(N, s(X)) :- N > 0, N0 is N - 1, n2s(N0, X).

down(s(X), X).

% Generate SK-combinator calculus terms of a given size.
untyped_sk(N, X) :- n2s(N, S), untyped_sk(X, S, z).

untyped_sk(s) --> [].
untyped_sk(k) --> [].
untyped_sk(a(X, Y)) -->
  down,
  untyped_sk(X),
  untyped_sk(Y).

% Count the number of SK-combinator calculus terms of a given size.
count_untyped(N, Count) :-
  aggregate_all(count, untyped_sk(N, _), Count).

% Print the counts of SK-combinator calculus terms of at most a given size.
%
%   ?- counts_untyped(10).
%   0: 2
%   1: 4
%   2: 16
%   3: 80
%   4: 448
%   5: 2688
%   6: 16896
%   7: 109824
%   8: 732160
%   9: 4978688
%   10: 34398208
%   true.
%
% https://oeis.org/A025225
counts_untyped(Max) :-
  between(0, Max, N),
  count_untyped(N, Count),
  format('~d: ~d~n', [N, Count]),
  fail.
counts_untyped(_).

% Test if `untyped_sk` generates SK-combinator calculus terms of the correct
% size. Should print the same output as `counts_untyped`.
test_untyped_sk(Max) :-
  between(0, Max, N),
  test_untyped_sk(N, Count),
  format('~d: ~d~n', [N, Count]),
  fail.
test_untyped_sk(_).

test_untyped_sk(N, Count) :-
  count_untyped(N, Count),
  aggregate_all(count, (untyped_sk(N, X), size(X, N)), Count).

% Pretty print an SK-combinator calculus term.
pretty(X) :-
  numbervars(X, 0, _),
  pretty(X, Xs, []),
  maplist(write, Xs),
  nl.

pretty(s) --> [s].
pretty(k) --> [k].
pretty(a(X, Y)) --> ['('], pretty(X), [' '], pretty(Y), [')'].

% Pretty print a type.
pretty_type(A) :-
  numbervars(A, 0, _),
  pretty_type(A, As, []),
  maplist(write, As),
  nl.

pretty_type(A -> B) -->
  ['('], pretty_type(A), !, [' → '], pretty_type(B), [')'].
pretty_type(A) --> [A].

% Print all SK-combinator calculus terms of a given size.
show_untyped(N) :-
  untyped_sk(N, X),
  pretty(X),
  fail.
show_untyped(_).

% Infer the type of a SK-combinator calculus term.
%
% The soundness and completeness of `infer` was tested against GHC's type
% checker. For every term of at most size 7, `infer` gives it a type if and
% only if GHC's type checker gives it the same type.
infer(s, (A -> B -> C) -> (A -> B) -> A -> C).
infer(k, A -> _B -> A).
infer(a(X, Y), B) :-
  infer(X, A -> B),
  infer(Y, A0),
  unify_with_occurs_check(A0, A).

% Generate typable SK-combinator calculus terms of a given size.
sk(N, X) :- n2s(N, S), sk(X, _, S, z).
sk(N, X, A) :- n2s(N, S), sk(X, A, S, z).

sk(s, (A -> B -> C) -> (A -> B) -> A -> C) --> [].
sk(k, A -> _B -> A) --> [].
sk(a(X, Y), B) -->
  down,
  sk(X, A -> B),
  sk(Y, A0),
  { unify_with_occurs_check(A0, A) }.

% Count the number of typable SK-combinator calculus terms of a given size.
count(N, Count) :-
  aggregate_all(count, sk(N, _), Count).

% Print the counts of typable SK-combinator calculus terms of at most a given
% size.
%
%   ?- counts(10).
%   0: 2
%   1: 4
%   2: 14
%   3: 67
%   4: 337
%   5: 1867
%   6: 10699
%   7: 63567
%   8: 387080
%   9: 2401657
%   10: 15145554
%   true.
%
counts(Max) :-
  between(0, Max, N),
  count(N, Count),
  format('~d: ~d~n', [N, Count]),
  fail.
counts(_).

% Test if `sk` generates SK-combinator calculus terms of the correct size and
% type. Should print the same output as `counts`.
test_sk(Max) :-
  between(0, Max, N),
  test_sk(N, Count),
  format('~d: ~d~n', [N, Count]),
  fail.
test_sk(_).

test_sk(N, Count) :-
  count(N, Count),
  aggregate_all(count, (sk(N, X, A), size(X, N), infer(X, A)), Count).

% Print all typable SK-combinator calculus terms of a given size.
show(N) :-
  sk(N, X, A),
  pretty(X),
  pretty_type(A),
  fail.
show(_).

main :-
  between(0, 7, N),
  show(N),
  fail.
main.