mix tptp.census (Tptp v0.1.0)

Copy Markdown View Source

Read every problem and axiom file of a local TPTP library and count where it applies a type constructor — list($i), map(A, B), tree @ $i — and in which dialects.

mix tptp.census
mix tptp.census --check

TPTP's type grammar admits type application: <tff_atomic_type> ::= <type_functor>(<tff_type_arguments>) and, in THF, an apply spine in type position. Whether the library actually uses it, how widely and in which dialects, is a fact worth having written down rather than guessed. The report is committed and kept current the way reports/CORPUS.md is: counts, not conclusions.

What is exact and what is a heuristic

A <tff_atomic_type> node is only ever built for an application, so the TFF count is exact. THF does not separate a type from a term — <thf_unitary_type> ::= <thf_unitary_formula> — so the THF figure is a heuristic: an apply spine inside a type-role statement. It is reported on its own line.

A file counts as outside the base languages when its dialect is none of cnf, fof, tf0 and th0, that is, when it requires polymorphism, arithmetic or a higher-order feature. That count refines the TFF row and only the TFF row: it is taken over the files an exact <tff_atomic_type> was found in, so it says nothing about the heuristic's files.

The heuristic's files are instead broken down by dialect, which indicates whether it is identifying types. An all-TH1 distribution indicates that it is; any TH0 in the distribution indicates that it is matching something other than polymorphism.

The constructor table is TFF only

record_thf/3 sets a boolean and never populates constructors. The names, arities and domains below therefore come from the exact TFF walk alone, and the heuristic's files contribute none of them — fun, list and option are not a census of the library's type constructors, they are a census of the ones TFF spells in a form the grammar makes unambiguous.

Arity 2 over a type variable

A constructor applied at arity 1, or at any arity over ground arguments, can be monomorphised into a fresh sort by an elaborator: list($i) is a sort. A constructor applied at arity ≥ 2 with a type variable among its arguments cannot be — fun(A, B) has to enter type unification as a constructor. That is a fork in the road for anything built on this library, so it is counted, twice: once for a variable as a direct argument, once for a variable anywhere beneath one, since fun(list(A), $i) is no more monomorphisable than fun(A, B) and the gap between the two counts is how much nesting the library actually does.

Reading the library

Each file is read with Tptp.from_string/2 and nothing else, exactly as mix tptp.corpus does; the same 20 MB size cap keeps the enormous axiom sets out. Run it separately: it performs one pass over the whole library.

Options

  • --every N — sweep one file in N. The full sweep is the default.
  • --timeout MS — per-file budget, default 60 s, as mix tptp.corpus.
  • --max-bytes N — skip files larger than this, default 20 MB.
  • --concurrency N — workers in the smallest size tier, default 4.
  • --heap BYTES — peak heap across all workers, default 6 GB. See mix help tptp.corpus for why the budget is heap rather than bytes of source.
  • --out PATH — where to write, default reports/CENSUS.md.
  • --check — write nothing; fail if the committed report's results differ from this run's.

Summary

Types

t()

What one sweep found.

Functions

census(paths, options \\ [])

Sweep a list of problem and axiom paths and total up the type application in them.

render(totals, run)

Render the committed report from a set of totals and the run metadata.

Types

t()

@type t() :: %{
  scanned: non_neg_integer(),
  tff_applied: non_neg_integer(),
  applied_outside_base: non_neg_integer(),
  var_direct: non_neg_integer(),
  var_nested: non_neg_integer(),
  thf_applied_heuristic: non_neg_integer(),
  thf_dialects: %{optional(Tptp.Query.dialect()) => non_neg_integer()},
  type_forall: non_neg_integer(),
  constructors: %{
    optional(binary()) => %{
      arities: [non_neg_integer()],
      domains: [binary()],
      files: non_neg_integer(),
      var_direct: non_neg_integer(),
      var_nested: non_neg_integer()
    }
  }
}

What one sweep found.

  • scanned — files read, parse failures included.
  • tff_applied — files with at least one applied <tff_atomic_type>.
  • applied_outside_base — of the TFF applied files, those whose dialect is not a base language.
  • var_direct — of the TFF applied files, those applying a constructor at arity ≥ 2 with a type variable as a direct argument.
  • var_nested — the same, counting a type variable anywhere beneath an argument. var_direct is a subset of it.
  • thf_applied_heuristic — files with an apply spine in a THF type position.
  • thf_dialects — those files by dialect, indicating whether the heuristic is identifying types.
  • type_forall — files using !>.
  • constructors — each TFF type constructor seen, with the arities it was applied at, the domains it appeared in, how many files used it, and in how many of those it took a type variable at arity ≥ 2, directly and nested.

Functions

census(paths, options \\ [])

@spec census(
  [Path.t()],
  keyword()
) :: t()

Sweep a list of problem and axiom paths and total up the type application in them.

Each path is read with Tptp.from_string/2; a file that does not parse still counts toward scanned and contributes nothing else.

render(totals, run)

@spec render(t(), %{
  root: Path.t(),
  every: pos_integer(),
  elapsed: non_neg_integer(),
  tiers: [{pos_integer(), pos_integer(), [Path.t()]}]
}) :: binary()

Render the committed report from a set of totals and the run metadata.