swipl_stt_judgements3.pl

:- module(swipl_stt,[substitute/4, '#'/2]).
:- use_module(library(gensym)).
:- op(999, xfx, user:'#').
:- op(998, xfx, user:'~>').	% one step normalization
:- op(998, xfx, user:'~>>').	% full normalization




% CAPTURE-AVOIDING SUBSTITUTION
substitute(X, Y, For,  X_Sub) :-
	var(X),
	!,
	(
		X == Y
	->	X_Sub = For
	;	X_Sub = X
	).
	
substitute([], _, _, []) :- !.
substitute([Term | Rest], X, For, [Term_Sub | Rest_Sub]) :-
	!,
	substitute(Term, X, For, Term_Sub),
	substitute(Rest, X, For, Rest_Sub).
	
substitute(bind(X,Expr), Y, For, bind(Fresh,Expr_Sub)) :-
	!,
	substitute(Expr, X, Fresh, Expr_Fresh),
	substitute(Expr_Fresh, Y, For, Expr_Sub).

substitute(Term, X, For, Term_Sub) :-
	Term =.. [F | Args],
	substitute(Args, X, For, Args_Sub),
	Term_Sub =.. [F | Args_Sub].


% HYPOTHESIS RULE
[X:T|_] # X:T.
[X:_|G] # Y:T :- X \= Y, G # Y:T.



% EMPTY / FALSE type  ; nullary sum
% formation
_ # type(empty).

% introduction
% -- no introduction rules!

% elimination
G # explosion(F):C :- 
	G # F:empty,
	G # type(C).

% beta?
% -- no beta rules because no introduction rules

% eta?
G # explosion(F) ~> F :-
	G # F:empty.


/*
* Notes:
* They use "abort_C" instead of "explosion" on ncatlab: https://ncatlab.org/nlab/show/empty+type
*  but, why should the label for the eliminator vary depending on the type that it's eliminating into?
*  We don't do this for any of the other types ex.. `unit_elim`, `if_then_else`, `case`, `apply`, ...
* 
* It seems to be implying that we need a different abort_C for every type C to make sure that the object
* abort_C(F) / explosion_C(F) actually has type C, and since there are different types we can't have the
* same abort_C on the same object F for every C... but... if we have a proof of False then the system is
* inconsistent and all the types should reduce to each other anyway, i.e. explosion(F) has every type in
* any context where F:empty
*
* They also have a different eta rule, i.e. abort_C(F):C <--eta--> c:C for any c:C;
* this should be logically equivalent to my F <--eta--> explosion(F) though, by similar logic as above?
*
*
* Trying to do proof-search by running bidirectionally: it immediately loops on the eliminator here
* (funny enough that means its search strategy is to try to prove everything via proving the logic
*  inconsistent...)
*
*/







% UNIT / TRUE / TOP / 1-member type ; nullary product
% formation
_ # type(unit).

% introduction
_ # null:unit.

% elimination
G # unit_elim(U, X):C :-
	G # U:unit,
	G # type(C),
	G # X:C.

% beta
_ # unit_elim(null, X) ~> X.

% eta
G # unit_elim(U,null) ~> U :-
	G # U:unit.







% BOOL / 2-member type
% formation
_ # type(bool).

% introduction
_ # true:bool.
_ # false:bool.

% elimination
G # if_then_else(B, X, Y):C :-
	G # B:bool,
	G # type(C),
	G # X:C,
	G # Y:C.

% beta
_ # if_then_else(true, X, _) ~> X.
_ # if_then_else(false, _, Y) ~> Y.

% eta
G # if_then_else(B, true, false) ~> B :-
	G # B:bool.

/*
* Notes:
* Can construct any finite enumeration type in similar fashion, but we can't construct
* the actual type *family* of finite enumerations, i.e. `Fin`, due to lack of dependent types.
*
*/





/*
% PAIR / PRODUCT / CONJUNCTION / "AND" type
% formation
judgement(type(pair(A,B)), G) :- 
	judgement(type(A), G),
	judgement(type(B), G).


% introduction
judgement((X,Y):pair(A,B), G) :- 
	judgement(type(pair(A,B)), G),
	judgement(X:A, G),
	judgement(Y:B, G).

% elimination
judgement(first(P):A, G) :- 
	judgement(P:pair(A,_), G).

judgement(second(P):B, G) :- 
	judgement(P:pair(_,B), G).

% beta
judgement(first((X,_)) = X, _).
judgement(second((_,Y)) = Y, _).

% eta
judgement(P = (first(P), second(P)), G) :-
	judgement(P:pair(_,_), G).
*/






/*
% DISJOINT UNION / DISJUNCTION / "OR" TYPE

% formation
judgement(type(union(A, B)), G) :- 
	judgement(type(A), G),
	judgement(type(B), G).

% introduction
judgement(left(X):union(A, B), G) :- 
	judgement(type(union(A, B)), G),
	judgement(X:A, G).

judgement(right(Y):union(A,B), G) :- 
	judgement(type(union(A,B)), G),
	judgement(Y:B, G).

% elimination
judgement(case(P, bind(x(V),L), bind(x(W),R)):C, G) :- 
	judgement(P:union(A,B), G),
	judgement(type(C), G),
	judgement(L:C, [x(V):A | G]),
	judgement(R:C, [x(W):B | G]).

% beta
judgement(case(left(X), bind(x(V),L), _) = LSub, _) :-
	substitute(L, x(V), X, LSub).
judgement(case(right(Y), _, bind(x(V),R)) = RSub, _) :-
	substitute(R, x(V), Y, RSub).


% eta
judgement(C = case(C, bind(x(V),left(x(V))), bind(x(W),right(x(W)))), G) :-
	judgement(C:union(_,_), G).
*/





/*
% IMPLICATION / FUNCTION TYPE
% formation
judgement(type(function(A, B)), G) :- 
	judgement(type(A), G),
	judgement(type(B), G).

% introduction
judgement(lambda(bind(x(V),Expr)):function(A,B), G) :- 
	judgement(type(function(A,B)), G),
	judgement(Expr:B, [ x(V):A | G]).

% elimination
judgement(apply(F,X):B,  G) :- 
	judgement(F:function(A,B), G),
	judgement(X:A, G).


% beta
judgement(apply(lambda(bind(x(V), Expr)), X) = FX, _) :-
	substitute(Expr, x(V), X, FX).

% eta
judgement(F = lambda(bind(x(V),apply(F,x(V)))), G) :-
	judgement(F:function(_,_),G).

*/




/*
% NATURAL NUMBERS
% formation
judgement(type(nat), _).

% introduction
judgement(0:nat, _).
judgement(suc(N):nat, G) :-
	judgement(N:nat, G).

% elimination
judgement(nat_rec(N,Z,bind(x(V),S)):C, G) :-
	judgement(N:nat, G),
	judgement(type(C), G),
	judgement(Z:C, G),
	judgement(S:C, [x(V):nat|G]).

% beta
judgement(nat_rec(0, Z, S) = Z, _).
judgement(nat_rec(suc(N), Z, bind(x(V),S)) = S_Sub, _) :-
	substitute(S, x(V), N, S_Sub).

% eta
judgement(N = nat_rec(N, 0, bind(x(V),suc(x(V)))), G) :-
	judgement(N:nat, G).

*/



/*
% LIST TYPE
% formation
judgement(type(list(A)), G) :-
	judgement(type(A), G).

% introduction
judgement([]:list(A), G) :-
	judgement(type(list(A)), G).
judgement([X | Xs]:list(A), G) :-
	judgement(type(list(A)), G),
	judgement(X:A, G),
	judgement(Xs:list(A), G).

% elimination
judgement(list_rec(L, Last, bind(x(V),bind(x(W),F))):C, G) :-
	judgement(type(C), G),
	judgement(L:list(_), G),
	judgement(Last:C, G),
	judgement(F:C, [x(V):list(A)|G]).


% beta
judgement(list_rec([], Nil, _) = Nil, _).
judgement(list_rec([X|Xs], _, bind(x(V),bind(x(W),Cons))) = Cons_Sub, _) :-
	substitute(Cons, x(V), X, Cons_Sub1),
	substitute(Cons_Sub1, x(W), Xs, Cons_Sub).
% eta
judgement(L = list_rec(L, [], bind(x(V),bind(x(W),[x(V)|x(W)]))), G) :-
	judgement(L:list(_), G).

*/

/*
* Notes:
* Can make a Vector type for any N, just can't construct the type *family* itself due to
* lack of dependent types.
*
*/




/*
% CONGRUENCE RULE
judgement(T1 = T2, G) :-
	T =.. [F | Args],
	maplist([X,Y]>>judgement(X = Y, G), Args, Args_Reduced),
	T_Reduced =.. [F | Args_Reduced],
	(
		Args \= Args_Reduced
	->	judgement(T_Reduced = T_Out, G)
	;	T_Out = T_Reduced
	).
*/





example(X) :-
	beta_reduction(
		apply(
			apply(
				lambda(bind(x(1), lambda(bind(x(2), x(1))))),
				"hi"
			),
			"bye"
		),
		X
	).