rename tpi.lam, rm redundant one in misc

Author: tromp

AIT.lhs

@@ -21,7 +21,7 @@ Size in bits of an expression, assuming no free variables
 > instance Encodeable DB where
 >   encode z = prebin z "" where
 >     prebin (DBVar 0) s = '1':'0':s
->     prebin (DBVar i) s | i>0 = '1':(prebin (DBVar (i-1)) s)
+>     prebin (DBVar i) s | i>0 = '1':'1':(prebin (DBVar (i-1)) s)
 >     prebin (DBVar   _) _ = error "Negative de-Bruijn index"
 >     prebin (DBLam   e) s = '0':'0':(prebin e s)
 >     prebin (DBApp x y) s = '0':'1':(prebin x (prebin y s))

BLC.tex

@@ -722,7 +722,7 @@ \subsection{Functional Complexity}
 In the {\em simple} version, programs are terminated with
 $N=\Cnil$ and the result must equal $x$.
 In the {\em prefix} version, programs are terminated with unsolvable $\Omega$,
-and the result must $x$.
+and the result must equal $x$.
 In a former prefix definition, now considered unnecessarily complicated and renamed Kp, programs were not terminated,
 and the result had to equal the pair of $x$ and the remainder of the input.
 In all cases the complexity is conditional on zero or more terms $y_i$.

misc/pi.lam ait/pi.lam

@@ -17,22 +17,20 @@
 --         bn = b*n
 --       in           go    bn (a*n21+bn) (c*n21) (n+1)
 
+-- related: tpi.hs and tuple_numerals.lam
+
 \io. let
-  id = \x. x;
-  bit0 = \x0\x1. x0;
-  bit1 = \x0\x1. x1;
-  cons = \a\b\p. p a b;
-  -- Church numerals
-  C1 = id;
   Csucc = \n\f\x. f (n f x);
-  Cadd = \a\b\f\x. a f (b f x);
-  -- Tuple numerals
-  -- Tm x (Tn y) = if n < m then y (Tm-1-n x) else x (Tn-m y)
-  T1 = \x\f. f x;
   Tadd = \tm\tn\x. tm (tn x);
+  id = \x. x;
+  bit0 = \x\y. x;
+  bit1 = \x\y. y;
   CTmul = \c\t. c t;
   Tsub = \tm\tn\x. tm id (tn x);
+  Cadd  = \a\b\f\x. a f (b f x);
+  cons = \a\b\p. p a b;
 
+  -- 399+2 bits
   go = \Tb\Ta\Tc. let
       prod = \bit\Ta'\Cn. cons bit (go (Tadd Tb Tb) (Tadd Ta' Ta') Tc Cn) in
       (Tc (\_. prod bit1 (Tsub Tc Ta)))      -- case Ta >= Tc
@@ -45,5 +43,21 @@
          (Ta (Tb (\_. prod bit0 Ta)))        -- case Ta+Tb < Tc
       ));
 
+  C1 = id;
+  T1 = \x\f. f x;
   pi = go T1 T1 T1 C1;
-in pi
+
+  -- YOLO, 376+2 bits
+  step = \cont\Tb\Ta\Tc\Cn.
+      let
+          x2np1 = CTmul (Csucc (Cadd Cn Cn));
+          CnxTb = CTmul Cn Tb
+      in  cont CnxTb (x2np1 (Tadd Ta Tb)) (x2np1 Tc) (Csucc Cn);
+  go_ = step (step (\Tb\Ta\Tc. let
+      prod = \bit\Ta'\Cn. cons bit (go_ (Tadd Tb Tb) (Tadd Ta' Ta') Tc Cn) in
+      (Tc (\_. prod bit1 (Tsub Tc Ta)))      -- case Ta >= Tc
+      (Ta (\_. prod bit0 Ta))));             -- case Ta < Tc
+  T0 = \x. x;
+  pi_probably = go_ T1 T0 T1 C1;
+in
+  pi

ait/tpi.lam

@@ -1,21 +1,87 @@
 $z=pop=~/8/;
 
-sub bit2lam {my$c=pop;sub{my$x=pop;sub{$c?pop:$x}}}
-sub byte2lam {my($c,$x)=@_;sub{$x--?
- pop->(bit2lam(vec$c,$x,1))->(byte2lam($c,$x)):sub{pop}}}
-sub input {my$i=pop;sub{my$c;($B[$i]||=defined($c=getc)?sub{pop->($z?
- byte2lam($c,8):bit2lam($c))->(input($i+1))}:sub{sub{pop}})->(pop)}}
-
-sub lam2bit {pop->(sub{0})->(sub{1})->()}
-sub lam2byte {my$x=pop;pop->(sub{$x=2*$x+lam2bit(pop);
- sub{my$r=pop;sub{lam2byte($r,$x)}}})->(chr$x)}
-sub output {pop->(sub{print($z?lam2byte(pop,0):lam2bit(pop));
- sub{my$r=pop;sub{output($r)}}})->("\n")}
-
-sub getbit {$x||=($c=getc,$z?8:1);vec$c,--$x,1}
-sub program {if(getbit()){my$i;$i++while getbit();sub{$_[$i]}}
- elsif(getbit()){my$p=program();my$q=program();sub{my@bit2lam
- =@_;$p->(@bit2lam)->(sub{$q->(@bit2lam)->(pop)})}}else{my$p=
- program();sub{my@bit2lam=@_;sub{$p->(pop,@bit2lam)}}}}
-
-$|=1; print output program()->()->(input(0))
+sub bit2lam {
+  my $bit = pop;
+  sub {
+    my $x0 = pop;
+      sub {
+        my $x1 = pop;
+        $bit ? $x1 : $x0
+      }
+  }
+}
+
+sub byte2lam {
+  my ($bits,$n) = @_;
+  sub {
+    $n-- ? pop->(bit2lam(vec$bits,$n,1))->(byte2lam($bits,$n)) # cons bitn bits>n
+         : sub { pop }                                         # nil
+  }
+}
+
+sub input {
+  my $n = pop;                                # input from n'th character onward
+  sub {
+    my $c;
+    ($B[$n] ||= defined($c=getc) ?
+       sub { pop->($z ? byte2lam($c,8) : bit2lam($c))->(input($n+1)) # cons charn chars>n
+       } :
+       sub { sub { pop } }                                           # nil
+    )->(pop)
+  }
+}
+
+sub lam2bit {
+  pop->(sub{0})->(sub{1})->()              # force suspension
+}
+
+sub lam2byte {
+  my $x = pop;	                           # 2nd argument is partial byte
+  pop->(sub {
+          $x = 2*$x + lam2bit(pop);
+          sub {
+            my $tail = pop;
+            sub { lam2byte($tail, $x) }
+          }
+        })->(chr $x)                       # end of byte
+}
+
+sub output {
+  pop->(sub {                              # more chars
+          my $c = pop;
+          print($z ? lam2byte($c,0) : lam2bit($c));
+          sub {
+            my $tail = pop;
+            sub { output($tail) }
+          }
+        })->(0)                         # end of output
+}
+
+sub getbit {
+  $n ||= ($c = getc, $z?8:1);
+  vec $c,--$n,1
+}
+
+sub program {
+  if (getbit()) {             # variable
+    my $i;
+    $i++ while getbit();
+    sub { $_[$i] }
+  } elsif (getbit()) {        # application
+    my $p=program();
+    my $q=program();
+    sub {
+      my @env = @_;
+      $p->(@env)->(sub { $q->(@env)->(pop) }) # suspend argument
+    }
+  } else {
+    my $p = program();
+    sub {
+      my @env = @_;
+      sub { $p->(pop,@env) }  # extend environment with one more argument
+    }
+  }
+}
+
+$| = 1;                                      # non zero value sets autoflush
+output program()->()->(input(0))             # run program with empty env on input

blc.pl

@@ -192,6 +192,8 @@ u32 evac(u32 n) {
   if (y == 'K') {
     mem[n+1] = mem[x+1];
     x = mem[n] = 'I';
+  } else if (y == 'F') {
+    x = mem[n] = 'I';
   }
   y = mem[n + 1];
   if (!x) return y;