Dataprops

A prop is similar to a type. If a prop is assigned to a dynamic term, then the term is guaranteed to be pure and total, that is, the evaluation of the term generates no effects and always terminates. We refer to dynamic terms classified by props as proof terms, or simply proofs. Dataprops are often declared for encoding recursively defined relations. For instance, multiplication on integers can be defined as follows in terms of integer addition:


0 n*	=	0
(m+1) n*	=	m n + n*	; if m >= 0
m n*	=	-(-m n)*	; if m < 0

Let MUL(m, n, p) be a relation on integers such that MUL(m, n, p) holds if and only if m * n = p. Then this relation can be encoded by the followng dataprop:

dataprop MUL (int, int, int) =
  | {n:int} MULbas (0, n, 0)
  | {m,n,p:int | m >= 0} MULind (m+1, n, p+n) of MUL (m, n, p)
  | {m,n,p:int | m > 0} MULneg (~m, n, ~p) of MUL (m, n, p)
// end of [MUL]

Proposition (Totality) For each pair of integers m and n, there exists an integer p such that m * n = p holds.

This proposition can be encoded as the following prop in ATS:

{m,n:int} () -< prf > [p:int] MUL (m, n, p)

which is assigned to the function MULprop_total defined below:

prfun MULprop_total
  {m,n:int}
  .< max(2*m,~2*m+1) >.
  (): [p:int] MUL (m, n, p) =
  sif m > 0 then MULind (MULprop_total {m-1,n} ())
  else sif m < 0 then MULneg (MULprop_total {~m,n} ())
  else MULbas ()
// end of [MULprop_total]

Note that we use sif for constructing a static conditional in which the condition is a static proposition, that is, a static term of sort bool. The conditions for the two occurrences of sif are m > 0 and m < 0, which are both static propositions.

Given that the prop {m,n:int} () -< prf > [p:int] MUL (m, n, p) is inhabited, we know that the proposition it encodes must hold.

Proposition (Uniqueness) Given integers m,n,p1,p2 such that m * n = p1 and m * n = p2, then p1 = p2 holds.

This proposition can be encoded as the following prop in ATS:

{m,n,p1,p2:int} (MUL (m, n, p1), MUL (m, n, p2)) -< prf > [p1 == p2] void

which is assigned to the function MULprop_unique defined below:

prfun MULprop_unique
  {m,n,p1,p2:int} .< max(2*m, ~2*m+1) >.
  (pf1: MUL (m, n, p1), pf2: MUL (m, n, p2)): [p1 == p2] void =
  case+ (pf1, pf2) of
    | (MULbas (), MULbas ()) => ()
    | (MULind pf1, MULind pf2) => MULprop_unique (pf1, pf2)
    | (MULneg pf1, MULneg pf2) => MULprop_unique (pf1, pf2)
// end of [MULprop_unique]

Therefore, the prop is inhabited and thus the proposition it encodes must hold.

The distributivity (over addition), commutativity and associativity of multiplication can all be esstablished similarly.

The code used for illustration is available here.