Higher-order Logic Programming

Executable Specification

[View higher-order.sig] [View higher-order.mod]
sig higher-order.

kind    a, alist        type.

type    anil            alist.
type    acons           a -> alist -> alist.

type    mappred         (a -> a -> o) -> alist -> alist -> o.

type    swap            (a -> a -> o) -> (a -> a -> o).

type    star            (a -> a -> o) -> (a -> a -> o).

% We don't have these explicitly in Abella, but we can define them
type    and             o -> o -> o.
type    exist           (a -> o) -> o.

module higher-order.

exist P :- P X.
and P Q :- P, Q.

mappred P anil anil.
mappred P (acons X XS) (acons Y YS) :- P X Y, mappred P XS YS.

swap P X Y :- P Y X.

star P X X.
star P X Y :- P X Z, star P Z Y.


[View higher-order.thm]

Click on a command or tactic to see a detailed view of its use.

%% This development is currently limited by the lack of polymorphism

Specification "higher-order".

Theorem split :
  forall R S L K,
    {mappred (x\ y\ exist z\ and (R x z) (S z y)) L K} ->
      exists J, {mappred R L J} /\ {mappred S J K}.

Theorem combine :
  forall R S L K J,
    {mappred R L J} -> {mappred S J K} ->
      {mappred (x\ y\ exist z\ and (R x z) (S z y)) L K}.

Theorem deterministic :
  forall R L K1 K2,
    (forall X Y1 Y2, {R X Y1} -> {R X Y2} -> Y1 = Y2) ->
      {mappred R L K1} -> {mappred R L K2} -> K1 = K2.

Theorem swap1 :
  forall R L K,
    {mappred (swap R) L K} -> {mappred R K L}.

Theorem swap2 :
  forall R L K,
    {mappred R K L} -> {mappred (swap R) L K}.

Define reflexive : (a -> a -> o) -> prop by
  reflexive P := forall X, {P X X}.

Define transitive : (a -> a -> o) -> prop by
  transitive P := forall X Y Z, {P X Y} -> {P Y Z} -> {P X Z}.

Theorem star_reflexive :
  forall P, reflexive (star P).

Theorem star_transitive :
  forall P, transitive (star P).

Define contained_in : (a -> a -> o) -> (a -> a -> o) -> prop by
  contained_in P S := forall X Y, {P X Y} -> {S X Y}.

% Theorem: star is minimal -- any reflexive and transitive relation
%  which contains P must contain (star P).
Theorem star_minimal :
  forall P S, contained_in P S -> reflexive S -> transitive S ->
    contained_in (star P) S.

% Corollary: if P is reflexive and transitive then (star P) equals P.
%  The easy direction is that (star P) contains P. The harder
%  direction is showing that P contains (star P). We do this harder
%  direction here.
Theorem star_vacuous :
  forall P, reflexive P -> transitive P -> contained_in (star P) P.

% Corollary: star is idempotent
Theorem star_idempotent :
  forall P, contained_in (star (star P)) (star P).