mstewartgallus/sequents.pro

## sequents.pro

:- use_module(library(clpfd)).
:- use_module(library(dcg/basics)).

:- op(1150, xfy, user:(———————————————————————————————————)).
:- op(980, xfy, user:(~~>)).
:- op(980, xfy, user:(~>)).
:- op(980, xfy, user:(*~>)).

:- op(950, xfx, user:(⊨)).
:- op(900, xfy, user:(⇓)).
:- op(900, xfy, user:(⇑)).

:- op(950, xfx, user:(⊢)).
:- op(850, xfy, user:(∈)).

:- op(800, xfy, user:(∘)).

:- op(800, xfy, user:(→)).
:- op(800, xfy, user:(←)).
:- op(750, xfy, user:(⇒)).
:- op(700, xfx, user:(×)).

:- op(750, xfy, user:(\)).

%% Grammar of types and terms

object(nat) --> [nat].
object(0) --> [0].
object(1) --> [1].
object(X × Y) --> ['×'], object(X), object(Y).
object(X + Y) --> ['+'], object(X), object(Y).
object(X ⇒ Y) --> ['⇒'], object(X), object(Y).

type(A → B) --> ['→'], object(A), object(B).

%% FIXME consider checking variables
term(id(A)) --> [id], object(A).
term(X ∘ Y) --> ['∘'], term(X), term(Y).

%% Variable rule
%% FIXME figure out variables later
term(v(N)) --> [v(N)].

%% Negative tuple terms
term(bang(A)) --> [bang], object(A).
term(fst(A)) --> [fst], object(A).
term(snd(A)) --> [snd], object(A).
term(fanout(A, B)) --> [fanout], term(A), term(B).

term(absurd(A)) --> [absurd], object(A).
term(inl(A)) --> [inl], object(A).
term(inr(A)) --> [inr], object(A).
term(fanin(A, B)) --> [fanin], term(A), term(B).

%% Positive function terms
term(force(X ∈ T, Body)) --> [force(X)], type(T), term(Body).
term(thunk(X)) --> [thunk], term(X).

%% Kappa calculus
term(kappa(X ∈ 1 → A, Body)) --> [kappa(X)], object(A), term(Body).
term(lift(A, X)) --> [lift], object(A), term(X).

%% Cokappa calculus
term(cokappa(X ∈ A → 0, Body)) --> [cokappa(X)], object(A), term(Body).
term(colift(A, X)) --> [colift], object(A), term(X).

%% Zeta calculus
term(zeta(X ∈ 1 → A, Body)) --> [zeta(X)], object(A), term(Body).
term(pass(A, X)) --> [pass], object(A), term(X).

%% Integer Extensions
term(z(N)) --> [z], integer(N).
term(add) --> [add].

%% FIXME check variables
item(X ∈ A → B) --> [item(X)], type(A → B).
environment([]) --> [].
environment([H | T]) --> item(H), environment(T).

is_type(X) :- phrase(type(X), _, []).
is_term(X) :- phrase(term(X), _, []).
is_type_env(X) :- phrase(environment(X), _, []).

%% Type Judgements

%% Category
true
———————————————————————————————————
Env ⊢ id(A) ∈ A → A.

Env ⊢ X ∈ B → C, Env ⊢ Y ∈ A → B
———————————————————————————————————
Env ⊢ X ∘ Y ∈ A → C.

%% Variable rule

(v(N) ∈ T) ∈ Env
———————————————————————————————————
Env ⊢ (v(N) ∈ T).

%% Terminal
true
———————————————————————————————————
_ ⊢ bang(A) ∈ A → 1.


%% Terminal
true
———————————————————————————————————
_ ⊢ absurd(A) ∈ 0 → A.

%% Kappa Calculus
Env ⊢ X ∈ 1 → A
———————————————————————————————————
Env ⊢ lift(B, X) ∈ B → (A × B).

[v(X) ∈ 1 → A | Env] ⊢ Body ∈ B → C
———————————————————————————————————
Env ⊢ kappa(X ∈ 1 → A, Body) ∈ (A × B) → C.

%% Cokappa Calculus
Env ⊢ X ∈ A → 0
———————————————————————————————————
Env ⊢ colift(B, X) ∈ (A + B) → B.

[v(X) ∈ A → 0 | Env] ⊢ Body ∈ C → B
———————————————————————————————————
Env ⊢ cokappa(X ∈ A → 0, Body) ∈ C → (A + B).

%% Zeta Calculus
Env ⊢ X ∈ 1 → A
———————————————————————————————————
Env ⊢ pass(B, X) ∈ (A ⇒ B) → B.

[v(X) ∈ 1 → A | Env] ⊢ Body ∈ B → C
———————————————————————————————————
Env ⊢ zeta(X ∈ 1 → A, Body) ∈ B → (A ⇒ C).

%% Negative rules for tuples
true
———————————————————————————————————
_ ⊢ fst(A) ∈ (A × B) → A.

true
———————————————————————————————————
_ ⊢ snd(B) ∈ (A × B) → B.

Env ⊢ X ∈ C → A, Env ⊢ Y ∈ C → B
———————————————————————————————————
Env ⊢ fanout(X, Y) ∈ C → (A × B).

%% Positive rules for functions
Env ⊢ X ∈ A → B
———————————————————————————————————
Env ⊢ thunk(X) ∈ 1 → (A ⇒ B).

[v(X) ∈ A → B | Env] ⊢ Body ∈ 1 → C
———————————————————————————————————
Env ⊢ force(X ∈ A → B, Body) ∈ (A ⇒ B) → C.

%% Integer extensions
true
———————————————————————————————————
_ ⊢ z(_) ∈ 1 → nat.

true
———————————————————————————————————
_ ⊢ add ∈ (nat × (nat × 1)) → nat.

%% Enforce variables are numbered 0 to N

bind(_, id(_)).
bind(N, F ∘ G) :- bind(N, F), bind(N, G).
bind(_, bang(_)).

bind(_, fst(_)).
bind(_, snd(_)).
bind(N, fanout(F, G)) :- bind(N, F), bind(N, G).

bind(_, inl(_)).
bind(_, inr(_)).
bind(N, fanin(F, G)) :- bind(N, F), bind(N, G).

bind(N, kappa(N ∈ 1 → A, Body)) :- bind(M, Body), M #= N + 1.
bind(N, lift(_, X)) :- bind(N, X).

bind(N, cokappa(N ∈ A → 0, Body)) :- bind(M, Body), M #= N + 1.
bind(N, colift(_, X)) :- bind(N, X).

bind(N, zeta(N ∈ 1 → A, Body)) :- bind(M, Body), M #= N + 1.
bind(N, pass(_, X)) :- bind(N, X).

bind(N, force(N ∈ A → B, Body)) :- bind(M, Body), M #= N + 1.
bind(N, thunk(X)) :- bind(N, X).

bind(_, v(_)).
bind(_, z(_)).
bind(_, add).


wellnumbered(Term) :- bind(0, Term).

%% Big Step Semantics

%% Category
true
———————————————————————————————————
_ ⊨ id(_) ⇓ X → X.

Env ⊨ G ⇓ X → Y,  Env ⊨ F ⇓ Y → Z
———————————————————————————————————
Env ⊨ F ∘ G ⇓ X → Z.

%% Variable Rule

(v(X) ⇓ T) ∈ Env
———————————————————————————————————
Env ⊨ v(X) ⇓ T.

%% Terminal

true
———————————————————————————————————
_ ⊨ bang(_) ⇓ _ → [].

true
———————————————————————————————————
_ ⊨ absurd(_) ⇓ _ → _.

%% Cartesian

true
———————————————————————————————————
_ ⊨ fst(_) ⇓ [X | _] → X.

true
———————————————————————————————————
_ ⊨ snd(_) ⇓ [_ | X] → X.

Env ⊨ F ⇓ X → L,  Env ⊨ G ⇓ X → R
———————————————————————————————————
Env ⊨ fanout(F, G) ⇓ X → [L | R].

%% Coproducts

true
———————————————————————————————————
_ ⊨ inl(_) ⇓ X → inl(X).

true
———————————————————————————————————
_ ⊨ inr(_) ⇓ X → inr(X).

Env ⊨ F ⇓ X → Y
———————————————————————————————————
Env ⊨ fanin(F, _) ⇓ inl(X) → Y.

Env ⊨ F ⇓ X → Y
———————————————————————————————————
Env ⊨ fanin(_, F) ⇓ inr(X) → Y.

%% Kappa calculus
[v(X) ⇓ [] → H | Env] ⊨ Body ⇓ T → Y
———————————————————————————————————
Env ⊨ kappa(X ∈ 1 → C, Body) ⇓ [H | T] → Y.

Env ⊨ F ⇓ [] → Y
———————————————————————————————————
Env ⊨ lift(_, F) ⇓ X → [Y | X].

%% Cokappa calculus
%% [v(X) ∈ A → 0 | Env] ⊢ Body ∈ C → B
%% ———————————————————————————————————
%% Env ⊢ cokappa(X ∈ A → 0, Body) ∈ C → (A + B).

[v(X) ⇓ H → _ | Env] ⊨ Body ⇓ Y → Z
———————————————————————————————————
Env ⊨ cokappa(X ∈ C → 0, Body) ⇓ Y → inl(H).

[v(X) ⇓ _ → _ | Env] ⊨ Body ⇓ Y → Z
———————————————————————————————————
Env ⊨ cokappa(X ∈ C → 0, Body) ⇓ Y → inr(Z).

Env ⊨ F ⇓ Y → X
———————————————————————————————————
Env ⊨ colift(_, F) ⇓ inl(Y) → X.

true
———————————————————————————————————
Env ⊨ colift(_, _) ⇓ inr(T) → T.


%% Zeta calculus

[v(X) ⇓ [] → H | Env] ⊨ Body ⇓ Y → Z
———————————————————————————————————
Env ⊨ zeta(X ∈ 1 → C, Body) ⇓ Y → fn(_, Z).

Env ⊨ F ⇓ [] → Y
———————————————————————————————————
Env ⊨ pass(_, F) ⇓ fn(_, Z) → Z.

%% Integer extras

true
———————————————————————————————————
_ ⊨ z(N) ⇓ [] → N.

{ Z #= X + Y }
———————————————————————————————————
_ ⊨ add ⇓ [X, Y] → Z.

%% Perhaps a sort of contravariant backwards bigstep relation can lead
%% to a simpler implementation?  Contravariance would turn universals
%% to existentials and vice-versa letting me treat function types
%% somewhat like products.

%% Variable Rule

(v(X) ⇓ [] → _) ∈ Env
———————————————————————————————————
Env ⊨ v(X) ⇑ _ ← _.

%% Category
true
———————————————————————————————————
_ ⊨ id(_) ⇑ X ← X.

Env ⊨ F ⇑ X ← Y, Env ⊨ G ⇑ Y ← Z
———————————————————————————————————
Env ⊨ F ∘ G ⇑ X ← Z.

%% Terminal
true
———————————————————————————————————
_ ⊨ bang(_) ⇑ _ → _.

true
———————————————————————————————————
_ ⊨ absurd(_) ⇑ _ ← [].

%% Products

true
———————————————————————————————————
_ ⊨ inl(_) ⇑ [X | _] ← X.

true
———————————————————————————————————
_ ⊨ inr(_) ⇑ [_ | X] ← X.

Env ⊨ F ⇑ X ← L,  Env ⊨ G ⇑ X ← R
———————————————————————————————————
Env ⊨ fanin(F, G) ⇑ X ← [L | R].

%% Coproducts

true
———————————————————————————————————
_ ⊨ fst(_) ⇑ X ← fst(X).

true
———————————————————————————————————
_ ⊨ snd(_) ⇑ X ← snd(X).

Env ⊨ F ⇑ Y ← X
———————————————————————————————————
Env ⊨ fanout(F, _) ⇑ fst(Y) ← X.

Env ⊨ F ⇑ Y ← X
———————————————————————————————————
Env ⊨ fanout(_, F) ⇑ snd(Y) ← X.

%% Kappa Calculus

%% [v(X) ⇑ H ← _ | Env] ⊨ Body ⇑ Y ← _
%% ———————————————————————————————————
%% Env ⊨ kappa(X ∈ 1 → C, Body) ⇑ Y ← fst(H).

%% [v(X) ⇑ _ ← _ | Env] ⊨ Body ⇑ _ ← T
%% ———————————————————————————————————
%% Env ⊨ kappa(X ∈ 1 → C, Body) ⇑ Y ← snd(T).

Env ⊨ F ⇑ Y ← X
———————————————————————————————————
Env ⊨ lift(_, F) ⇑ fst(Y) ← X.

%% like fanout(F, id(_))
true
———————————————————————————————————
_ ⊨ lift(_, _) ⇑ snd(X) ← X.

%% cokappa calculus

[v(X) ⇑ [] ← H | Env] ⊨ Body ⇑ T ← Y
———————————————————————————————————
Env ⊨ cokappa(X ∈ C → 0, Body) ⇑ [H | T] ← Y.

Env ⊨ F ⇑ [] ← Y
———————————————————————————————————
Env ⊨ colift(_, F) ⇑ X ← [Y | X].

%% Zeta calculus

[v(X) ⇓ [] → H | Env] ⊨ Body ⇑ T ← Y
———————————————————————————————————
Env ⊨ zeta(X ∈ 1 → C, Body) ⇑ fn(H, T) ← Y.

Env ⊨ F ⇓ [] → Y
———————————————————————————————————
Env ⊨ pass(_, F) ⇑ X ← fn(Y, X).

%% Integer extras

true
———————————————————————————————————
_ ⊨ z(_) ⇑ _ ← _.

true
———————————————————————————————————
_ ⊨ add ⇑ _ ← _.

%% Small Step Control flow Semantics

%% Meta Interpretation

inject(Program, Vars, ck(Program, Heap, [])) :-
    init_heap(Vars, Heap).

%% FIXME.. pull out more logic..
lookup(Env ⊨ F, Tail, S0, S1, Diff)
———————————————————————————————————
ck(Env ⊨ F, S0, Subs) ~> ck(Tail, S1, [Diff | Subs]).

unify(X, Y, S0, S1, Diff)
———————————————————————————————————
ck(X = Y, S0, Subs) ~> ck(true, S1, [Diff | Subs]).

true
———————————————————————————————————
ck((true, Rest), K, Subs) ~> ck(Rest, K, Subs).

%% Fixme.. problematic...
X ∈ Y
———————————————————————————————————
ck(X ∈ Y, Env, Subs) ~> ck(true, Env, Subs).

{ X }
———————————————————————————————————
ck({ X }, Env, Subs) ~> ck(true, Env, Subs).

ck(X, Env0, Subs0) ~> ck(Y, Env1, Subs1)
———————————————————————————————————
ck((X, Rest), Env0, Subs0) ~> ck((Y, Rest), Env1, Subs1).

ck(A, Env0, Subs0) ~> ck(X, Env1, Subs1)
———————————————————————————————————
ck((A ; B), Env0, Subs1) ~> ck((X ; B), Env1, Subs1).

true
———————————————————————————————————
ck((true ; _), Env, Subs) ~> ck(true, Env, Subs).

true
———————————————————————————————————
ck((false ; A), Env, Subs) ~> ck(A, Env, Subs).

%% Multi step semantics

%% IDK why the free path category showed up here
true
———————————————————————————————————
A ~~> A.

A ~> B, B ~~> C
———————————————————————————————————
A ~~> C.

%% Helper Rules

false
———————————————————————————————————
A ∈ [].

true
———————————————————————————————————
H ∈ [H | _].

H ∈ T
———————————————————————————————————
H ∈ [_ | T].

%% Search Judgements
judge(true) --> [true].
judge(false) --> { false }.
judge(A = B) --> [A = B], { A = B }.
judge((A, B)) --> [(A, B)], judge(A), judge(B).
judge(A ; _) --> [inl(A)], judge(A).
judge(_ ; A) --> [inr(A)], judge(A).
judge({ X }) --> [{ X }], { call(X) }.
judge(unify(X, Y, Store0, Store1, Diff)) -->
    [X = Y],
    {
        heap(M, Vars) = Store0,
        heap(N, NewVars) = Store1,
        Diff = Assoc,

        length(Vars, NumVars),
        length(FreshVars, NumVars),
        maplist(assoc, Assoc, Vars, FreshVars),
        substitute(Assoc, X = Y, A = B),
        A = B,
        term_variables(A, NewVars),
        numbervars(NewVars, M, N)
    }.
judge(lookup(Head, Tail, Store0, Store1, Diff)) -->
    [Head :- Tail],
    {
        heap(M, Vars) = Store0,
        heap(N, NewVars) = Store1,
        Diff = Assoc,

        length(Vars, NumVars),
        length(FreshVars, NumVars),
        maplist(assoc, Assoc, Vars, FreshVars),
        substitute(Assoc, Head, FreshHead),
        lookup(FreshHead, Tail),
        term_variables((FreshHead, Tail), NewVars),
        numbervars(NewVars, M, N)
    }.
judge(Head) -->
    [
        Tail
        ———————————————————————————————————
        Head
    ], {
        rule(Head),
        (
            Tail
            ———————————————————————————————————
            Head
        )
    }, judge(Tail).

init_heap(Vars, heap(N, Vars)) :-
    numbervars(Vars, 0, N).

%% quick nonlogical hack...
assoc(K = V, K, V).
substitute(Map, Key, Value) :-
    member(Key = Value, Map).
substitute(Term, Term) :- atom(Term).
substitute(Map, Term, Fresh) :-
    Term =.. [Head | Args],
    maplist(substitute(Map), Args, FreshArgs),
    Fresh =.. [Head | FreshArgs].

lookup(Head, Tail) :-
    clauses(Head, PossibleTails),

    %% Rewrite multiple tails as or'd together this lets the
    %% metainterpreter decide how to handle choices.
    orall(PossibleTails, Tail).


%% We use this odd format so as to explicitly reify head unification
clauses(Head, Clauses) :-
    findall((_ = Head, Tail),
            Tail
            ———————————————————————————————————
            Head,
            Clauses),
    maplist(head(Head), Clauses).

head(Head, (Head = _, _)).

orall(Choices, Clause) :-
    reverse(Choices, R),
    rev_orall(R, Clause).

%% We have to unroll slightly to avoid introducing a silly A;false at
%% the end
rev_orall([], false).
rev_orall([H | T], Out) :-
    foldl(or, T, H, Out).

or(X, Y, X ; Y).

rule(_ ∈ _).
rule(_ ⊨ _).
rule(_ ~> _).
rule(_ ~~> _).
rule(_ ⊢ _ ∈ _).

%% Put it all together

wellformed(Env ⊢ F ∈ T, Tree) :-
    phrase(judge(Env ⊢ F ∈ T), Tree),
    is_type(T),
    is_term(F),
    is_type_env(Env).

run(Env ⊨ F ⇓ X → Y ~~> Z, Proof) :-
    phrase(judge([] ⊨ alphaeq(F, Term)), _),
    wellnumbered(Term),
    phrase(judge((Env ⊨ Term ⇓ X → Y) ~~> Z), Proof).

%% program(
%%     kappa(X ∈ 1 → nat,
%%           add ∘
%%           lift(_, z(4)) ∘
%%           lift(_, v(X))) ∘
%%     lift(_, z(3))
%%     ).

%% program(
%%     kappa(X ∈ 1 → _, lift(_, v(X)) ∘ lift(_, v(X))) ∘
%%     lift(_, zeta(Y ∈ 1 → nat, add ∘ lift(_, v(Y)) ∘ lift(_, v(Y))))
%% ).

%% program(
%%     kappa(X ∈ 1 → nat,
%%     kappa(Y ∈ 1 → nat,
%%           lift(_, v(X)) ∘ lift(1, v(Y))))).

%% program(
%%     cokappa(K ∈ nat → 0, z(8))).

%% program(z(4)).

%% program(add ∘ lift(_, z(4)) ∘ lift(_, z(4))).
%% program(z(4)).
%% program(pass(_, z(4)) ∘ zeta(X ∈ 1 → nat, v(X))).

program(z(5)).
%% program(fanout(z(5), id(_))).
%% program(z(4)).


go(Halt) :-
    program(F),
    wellnumbered(F),

    wellformed([] ⊢ F ∈ _, _),

    P = ([] ⊨ F ⇓ X),
    %% phrase(judge(P), Proof),
    %% maplist(pp, Proof).

    Halt = ck(true, _, _),
    term_variables(P, Vars),
    inject(P, Vars, State0),
    findall(step(Halt,Proof), phrase(judge(State0 ~~> Halt), Proof), Steps),
    append(_, [Last], Steps),
    step(Halt, Proof) = Last,
    maplist(pp, Proof).

    %% include(escapes, Exec, Real).
    %% writeln(Y := proc(X)),
    %% maplist(pp, Real).

escapes({_}).

pp(true).
pp({A}) :-
    writeln({A}).
pp((A = B)) :-
    writeln(A = B).
pp((A, B)) :-
    pp(A),
    pp(B).
pp((A ; B)) :-
    writeln(A ; B).
pp(inl(A)) :-
    pp(A),
    writeln(inl).
pp(inr(A)) :-
    pp(A),
    writeln(inr).
%%% meta lookup
pp(Head :- Tail) :-
    writeln((Head :- Tail)).
pp(Tail
   ———————————————————————————————————
   Head)
:-
    pp(Tail),
    writeln(———————————————————————————————————),
    pp(Head),
    nl.
pp(X) :-
    rule(X),
    writeln(X).
pp(X) :-
    X = lookup(_, _, _, _, _),
    writeln(X).
pp(X) :-
    X = unify(_, _, _, _, _),
    writeln(X).

test :-
    test_fst,
    test_snd,
    test_zeta.

test_fst :-
    wellformed([] ⊢ fst(nat) ∈ (nat × 1) → nat).
test_snd :-
    wellformed([] ⊢ snd(nat) ∈ (1 × nat) → nat).

test_zeta :-
    wellformed([] ⊢ zeta(X ∈ 1 → nat, lift(nat, v(X))) ∈ nat → (nat ⇒ nat × nat)).