taus puzzle

enumerate.ts

import * as cp from 'child_process';

type Prop = 'a' | 'b' | [Prop, Prop];

function propToStr(p: Prop): string {
  if (typeof p === 'string') return p;
  return `im(${propToStr(p[0])}, ${propToStr(p[1])})`;
}

function propToStrIleancop(p: Prop): string {
  if (typeof p === 'string') return p;
  return `(${propToStrIleancop(p[0])} => ${propToStrIleancop(p[1])})`;
}

function imp(p: Prop, q: Prop): Prop {
  return [p, q];
}

function seen(c: Prop, old: Prop[]): number | undefined {
  for (const [ix, op] of old.entries()) {
    if (equiv(c, op))
      return ix;
  }
}

function fresh(c: Prop, old: Prop[]): boolean {
  return seen(c, old) === undefined;
}

function enumerateProps(old: Prop[]): Prop[] {
  const cand: Prop[] = [];
  const rv: Prop[] = [];
  old.forEach(p => {
    old.forEach(q => {
      cand.push(imp(p, q));
    });
  });
  cand.forEach(c => {
    if (fresh(c, old) && fresh(c, rv))
      rv.push(c);
  });
  return rv;
}

function tabulateProps(old: Prop[]): number[][] {
  return old.map(p =>
    old.map(q =>
      seen(imp(p, q), old)!
    )
  );
}

function equiv(p: Prop, q: Prop): boolean {
  return provable(imp(p, q)) && provable(imp(q, p));
}

const cache: { [k: string]: boolean } = {};

function provableIleancop(p: Prop): boolean {
  const propStr = propToStrIleancop(p);
  if (!(propStr in cache)) {
    console.log(`testing ${propStr}`);
    cache[propStr] = !cp.spawnSync('swipl', ['-g', `prove(${propStr})`, '-t', 'halt', '/tmp/ileancop_swi.pl']).status;
  }
  return cache[propStr];
}

// I added the predicate
// ```
// prove(X):-
// permanenzaSegno([swff(f,X)],StartingSet, _),
// orderEquivSet(StartingSet, OrderedStartingSet),
// reapply(OrderedStartingSet, _, 1, 1).
// ```
// to the swi-prolog file fCube found in fCube 11.1 from
//     http://www2.disco.unimib.it/fiorino/fcube.html
// and renamed it fCube.pl because swipl doesn't seem to want to
// run it properly without that extension.

function provable(p: Prop): boolean {
  const propStr = propToStr(p);
  if (!(propStr in cache)) {
    // console.log(`testing ${propToStrIleancop(p)}`);
    cache[propStr] = !!cp.spawnSync('swipl', ['-g', `prove(${propStr})`, '-t', 'halt', '/tmp/fCube.pl']).status;
  }
  return cache[propStr];
}

let known: Prop[] = ['a', 'b'];

for (let i = 0; i < 3; i++) {
  known = known.concat(enumerateProps(known));
}

for (const p of known) {
  console.log(propToStrIleancop(p));
}

console.log(JSON.stringify(tabulateProps(known), null, 2));