fork download
copy 
  1. typedef int Tree;
  2. typedef int INT;
  3. typedef int TREE;
  4. typedef int BitStream;
  5. #define DESCEND xx
  6.  
  7. Tree lastRight, accumulate;
  8.  
  9. // A bijective pairing.
  10. TREE Pair (TREE yy, TREE xx)
  11. {
  12.    // x - ~x = x - (-1 - x) = 2 * x + 1
  13.    return yy - ~yy << xx;
  14. }
  15.  
  16. // The second component of a pair.
  17. TREE Right (TREE xx)
  18. {
  19.    return lastRight = xx % 2 ? 0 : 1 + Right (xx / 2);
  20. }
  21.  
  22. // The first component.  Note that we leave the other component in lastRight.
  23. TREE Left (TREE xx)
  24. {
  25.    return xx / 2 >> Right (xx);
  26. }
  27.  
  28. // Encoding
  29. // PI(A,B) = Pair(0,Pair(A,B))
  30. // LAMBDA(A,B) = Pair(1,Pair(A,B))
  31. // APPLY(A,B) = Pair(2,Pair(A,B))
  32. // STAR = Pair(3,0) = 7
  33. // BOX = Pair(3,1) = 14
  34. // VAR(n) = Pair(4+2n,0) = 9 + 4n [n >= 0]
  35. // The empty context is 0, and the context Gamma,A is Pair (A,Gamma).
  36. // STAR and BOX are the only terms x with (x&2)!=0
  37.  
  38. // Increment the index of each variable in xx.  Uses Subst.
  39. // Making this a macro means that we can absorb an "=" and a "(" into the macro.
  40. #define Lift(xx) Subst (4, 13, -4, xx)
  41.  
  42. // Substitute yy for vv in term, and normalise.  Variables > yy get adjusted by
  43. // -context.  [The precise normalisation is: if yy and term are normal, and the
  44. // substitution has a normal form, then the normal form is returned.]
  45. TREE Subst (INT vv, TREE yy, INT context, TREE term)
  46. {
  47.    Tree
  48.       aux = Left (term),        // The operation of term.
  49.       xx = lastRight;           // The body of term.
  50.  
  51.    {
  52.       return
  53.          aux - 2 ?
  54.          aux > 2 ?
  55.          // Variable or Star or Box.
  56.          aux - vv ? term - (aux > vv) * context : yy :
  57.          // aux = 0 or aux = 1: lambda or pi.  The stray 'term =' below is
  58.          // harmless, but allows us to push the '=' into the Lift macro.
  59.          Pair (aux, Pair (Subst (vv, yy, context, Left (xx)),
  60.                           Subst (vv+2, term = Lift (yy), context, Right (xx))))
  61.          :
  62.          // Application.  Use Apply.
  63.          Apply (Subst (vv, yy, context, Left (xx)),
  64.                 Subst (vv, yy, context, Right (xx)));
  65.    }
  66. }
  67.  
  68. // Apply yy to xx and normalise.  [Precisely, if yy and xx are normal, and
  69. // yy(xx) is normalisable, Apply(yy,xx) returns the normal form of yy(xx).
  70. TREE Apply (TREE yy, TREE xx)
  71. {
  72.    return Left (yy) - 1
  73.       // 5 << x == Pair(2,x)
  74.       ? 5 << Pair (yy, xx)
  75.       : Subst (4, xx, 4, Right (lastRight));
  76. }
  77.  
  78. // We use xx as a bit stream.  The MAYBE macro tests the next bit for us.
  79. #define MAYBE (xx /= 2) % 2 &&
  80.  
  81. // Derive parses a bit stream into terms of CoC and normalises everything.  The
  82. // outputs are accumulated into the variable yy.  We also recurse, so as to
  83. // cover all the BitStreams which are < xx.
  84. TREE Derive (BitStream xx)
  85. {
  86.    Tree
  87.       aux,
  88.       auxTerm,
  89.       // The axiom.
  90.       context = 0,
  91.       term = 7,
  92.       type = 14;
  93.  
  94.    // Inside the while condition is the main recursion that makes us monotone.
  95.    // It doesn't need to be inside the while, but that allows us to compress the
  96.    // "),".  It also means we get called more often, which makes "accumulate"
  97.    // bigger...
  98.    while (DESCEND && Derive (xx - 1), MAYBE (1))
  99.  
  100.       // Get another term.
  101.       auxTerm = Left (Left (Derive (xx))),
  102.          // And get its type.
  103.          aux = Left (lastRight),
  104.  
  105.          // And get the left-over bit-stream.  This leaves the context from
  106.          // the sub-derivation in lastRight.
  107.          xx = Left (lastRight),
  108.  
  109.          // Rules that depend on two antecedents...  The two contexts (one is in
  110.          // lastRight) must be the same.
  111.          context - lastRight || (
  112.             // APPLY.  type must be PI(aux,-).
  113.             Left (type) || Left (lastRight) - aux ||
  114.             MAYBE (type = Subst (4, auxTerm, 4, lastRight),
  115.                    term = Apply (term, auxTerm)),
  116.  
  117.             // Weakening.  auxType must be STAR or BOX.  The / 2 & MAYBE
  118.             // combines MAYBE with testing the correct bit of auxType.  It is
  119.             // safe to do this immediately after an APPLY above, because APPLY
  120.             // does not change contexts.
  121.             aux / 2 & MAYBE ( context = Pair (auxTerm, context),
  122.                               term = Lift (term),
  123.                               type = Lift (type) )
  124.  
  125.             ),
  126.  
  127.          context && MAYBE (
  128.             // If we get here, we are either going to do PI formation or LAMBDA
  129.             // introduction.  PI formation requires type to be STAR or BOX.  We
  130.             // allow LAMBDA introduction whenever the context is non-empty.
  131.             // This extension is a conservative extension of CoC.
  132.             term = Pair (
  133.                // Because of the && in MAYBE, this subexpression returns a
  134.                // boolean 1 if we're doing LAMBDA introduction, 0 if we're
  135.                // doing PI formation.  The ~type&2| ensures that we do LAMBDA
  136.                // introduction if type is not the Star or Box needed to do PI
  137.                // formation.
  138.                ~type & 2 | MAYBE (
  139.                   // If we're doing lambda introduction on term, then we also
  140.                   // need to do a PI formation on type.  This is always
  141.                   // non-zero.  1 << x = Pair(0,x).
  142.                   type = 1 << Pair (Left (context), type)),
  143.                Pair (Left (context), term)),
  144.  
  145.             // Remove the context item we just used.
  146.             context = lastRight ),
  147.  
  148.          // If type is STAR or BOX then we allow variable introduction.
  149.          type / 2 & MAYBE (
  150.             context = Pair (term, context),
  151.             type = Lift (term),
  152.             term = 9 );     // Pair (4, 0)
  153.    {
  154.       // Pair term, type, context, and xx together, and chuck it all onto
  155.       // accumulate.
  156.       return accumulate = Pair (Pair (term, Pair (type, Pair (xx, context))),
  157.                                 accumulate);
  158.    }
  159. }
  160.  
  161. TREE main ()
  162. {
  163.    return Derive (2);
  164. }
Success #stdin #stdout 0.01s 5268KB
comments (?)
stdin
copy 
Standard input is empty
stdout
copy 
Standard output is empty
https://ideone.com/GNUxvn
language:
C (gcc 8.3)
created:
2 hours ago
visibility:
public

Share or Embed source code

Discover > Sphere Engine API

The brand new service which powers Ideone!

Discover > IDE Widget

Widget for compiling and running the source code in a web browser!