------------------------------------------------------------------------------ [The language of combinators in S, K, with variables taken from the set A] ------------------------------------------------------------------------------ ( A : ! ( X, Y : ! ! * ! ( a : A ! ( A : * ! ( A : * ! ! SK A ! data !------! where !--------! ; !--------! ; !--------! ; !---------! ! SK A ! ! V a : ! ! K : ! ! S : ! ! app X Y ! ! : * ) ! SK A ) ! SK A ) ! SK A ) ! : SK A ) ------------------------------------------------------------------------------ [a boring helper function] ------------------------------------------------------------------------------ ( X : SK A ! let !-------------! ! k1 X : SK A ) k1 X => app K X ------------------------------------------------------------------------------ [the K redex...] ------------------------------------------------------------------------------ ( X, Y : SK A ! let !--------------! ! k X Y : SK A ) k X Y => app (k1 X) Y ------------------------------------------------------------------------------ [... and its contractum] ------------------------------------------------------------------------------ ( X, Y : SK A ! let !---------------! ! k' X Y : SK A ) k' X Y => X ------------------------------------------------------------------------------ [another boring helper function...] ------------------------------------------------------------------------------ ( X : SK A ! let !-------------! ! s1 X : SK A ) s1 X => app S X ------------------------------------------------------------------------------ [... and another...] ------------------------------------------------------------------------------ ( X, Y : SK A ! let !---------------! ! s2 X Y : SK A ) s2 X Y => app (s1 X) Y ------------------------------------------------------------------------------ [... which defines the S redex...] ------------------------------------------------------------------------------ ( X, Y, Z : SK A ! let !----------------! ! s X Y Z : SK A ) s X Y Z => app (s2 X Y) Z ------------------------------------------------------------------------------ [... and its contractum. ] ------------------------------------------------------------------------------ ( X, Y, Z : SK A ! let !-----------------! ! s' X Y Z : SK A ) s' X Y Z => app (app X Z) (app Y Z) ------------------------------------------------------------------------------ [The Tait-Martin-Lof notion of parallel reduction for this language... ] ------------------------------------------------------------------------------ ( X, Y : SK A ! data !-------------! ! par X Y : * ) ( a : A ! where !--------------------------! ! parV a : par (V a) (V a) ) ( A : * ! !-------------------------------! ! parK _A : par (K _ A) (K _ A) ) ( A : * ! !-------------------------------! ! parS _A : par (S _ A) (S _ A) ) ( pX : par X X' ! ! ! ( pX : par X X' ! ! pY : par Y Y' ! ! ! ! ! ! pY : par Y Y' ! ( pX : par X X' ! ! pZ : par Z Z' ! !-----------------! ; !---------------! ; !-------------------! ! parapp pX pY : ! ! park pX : ! ! pars pX pY pZ : ! ! par (app X Y) ! ! par (k X Y) ! ! par (s X Y Z) ! ! % (app X' Y') ) ! % (k' X' Y) ) ! % (s' X' Y' Z') ) ------------------------------------------------------------------------------ [Booleans and their indicator type...] ------------------------------------------------------------------------------ data (--------! where TT, FF : BB ! BB : * ) ------------------------------------------------------------------------------ ( b : BB ! data !----------! where oh : So TT ! So b : * ) ------------------------------------------------------------------------------ [... with a laborious series of definitions of what it means to be...] ------------------------------------------------------------------------------ ( X : SK A ! let !--------------! ! notK0 X : BB ) notK0 X <= case X { notK0 (V a) => TT notK0 K => FF notK0 S => TT notK0 (app X Y) => TT } ------------------------------------------------------------------------------ ( X : SK A ! let !--------------! ! notK1 X : BB ) notK1 X <= case X { notK1 (V a) => TT notK1 K => TT notK1 S => TT notK1 (app X Y) => notK0 X } ------------------------------------------------------------------------------ ( X : SK A ! let !--------------! ! notK2 X : BB ) notK2 X <= case X { notK2 (V a) => TT notK2 K => TT notK2 S => TT notK2 (app X Y) => notK1 X } ------------------------------------------------------------------------------ [... not yielding a K redex when applied...] ------------------------------------------------------------------------------ ( X : SK A ! let !-------------! ! NotK1 X : * ) NotK1 X => So (notK1 X) ------------------------------------------------------------------------------ ( X : SK A ! let !-------------! ! NotK2 X : * ) NotK2 X => So (notK2 X) ------------------------------------------------------------------------------ ( X : SK A ! let !--------------! ! notS0 X : BB ) notS0 X <= case X { notS0 (V a) => TT notS0 K => TT notS0 S => FF notS0 (app X Y) => TT } ------------------------------------------------------------------------------ ( X : SK A ! let !--------------! ! notS1 X : BB ) notS1 X <= case X { notS1 (V a) => TT notS1 K => TT notS1 S => TT notS1 (app X Y) => notS0 X } ------------------------------------------------------------------------------ ( X : SK A ! let !--------------! ! notS2 X : BB ) notS2 X <= case X { notS2 (V a) => TT notS2 K => TT notS2 S => TT notS2 (app X Y) => notS1 X } ------------------------------------------------------------------------------ ( X : SK A ! let !--------------! ! notS3 X : BB ) notS3 X <= case X { notS3 (V a) => TT notS3 K => TT notS3 S => TT notS3 (app X Y) => notS2 X } ------------------------------------------------------------------------------ [... and not yielding an S redex when applied] ------------------------------------------------------------------------------ ( X : SK A ! let !-------------! ! NotS2 X : * ) NotS2 X => So (notS2 X) ------------------------------------------------------------------------------ ( X : SK A ! let !-------------! ! NotS3 X : * ) NotS3 X => So (notS3 X) ------------------------------------------------------------------------------ [complete development: parallel reduction with non-overlapping rules] ------------------------------------------------------------------------------ ( X, Y : SK A ! data !-------------! ! dev X Y : * ) ( a : A ! where !--------------------------! ! devV a : dev (V a) (V a) ) ( A : * ! !-------------------------------! ! devK _A : dev (K _ A) (K _ A) ) ( A : * ! !-------------------------------! ! devS _A : dev (S _ A) (S _ A) ) ( dX : dev X X' ; dY : dev Y Y' ; nK : NotK1 X ; nS : NotS2 X ! !----------------------------------------------------------------! ! devapp dX dY nK nS : dev (app X Y) (app X' Y') ) ( dX : dev X X' ! ( dX : dev X X' ; dY : dev Y Y' ; dZ : dev Z Z' ! !---------------! ; !-------------------------------------------------! ! devk dX : ! ! devs dX dY dZ : dev (s X Y Z) (s' X' Y' Z') ) ! dev (k X Y) ! ! % (k' X' Y) ) ------------------------------------------------------------------------------ [Finally, the Takahashi triangle lemma] ------------------------------------------------------------------------------ ( d : dev M N ; p : par M P ! let !----------------------------! ! takahashi d p : par P N ) takahashi d p <= rec d { takahashi d p <= case d { takahashi (devV a) p <= case p { takahashi (devV a) (parV a) => parV a } takahashi devK p <= case p { takahashi devK parK => parK } takahashi devS p <= case p { takahashi devS parS => parS } takahashi (devapp dM dN nK nS) p <= case p { takahashi (devapp dM dN nK nS) (parapp pX pP) => parapp (takahashi dM pX) (takahashi dN pP) takahashi (devapp dM dN nK nS) (park pP) <= case nK takahashi (devapp dM dN nK nS) (pars pX pP pZ) <= case nS } takahashi (devk dN) p <= case p { takahashi (devk dN) (parapp pX pP) <= case pX { takahashi (devk dN) (parapp (parapp pXX pXX') pP) <= case pXX { takahashi (devk dN) (parapp (parapp parK pXX') pP) => park (takahashi dN pXX') } } takahashi (devk dN) (park pX) => takahashi dN pX } takahashi (devs dM dN dZ) p <= case p { takahashi (devs dM dN dZ) (parapp pX pP) <= case pX { takahashi (devs dM dN dZ) (parapp (parapp pXX pXX') pP) <= case pXX { takahashi (devs dM dN dZ) % (parapp (parapp (parapp pXXX pXXX') pXX') pP) <= case pXXX { takahashi (devs dM dN dZ) % (parapp (parapp (parapp parS pXXX') pXX') pP) => pars (takahashi dM pXXX') (takahashi dN pXX') % (takahashi dZ pP) } } } takahashi (devs dM dN dZ) (pars pX pP pZ) => parapp (parapp (takahashi dM pX) (takahashi dZ pZ)) % (parapp (takahashi dN pP) (takahashi dZ pZ)) } } } ------------------------------------------------------------------------------