Type application census

Where a local TPTP library applies a type constructor, and in which dialects. Every problem and axiom file is read with Tptp.from_string/2 and nothing else, under the same 20 MB size cap as mix tptp.corpus.

The TFF count is exact — a <tff_atomic_type> node is only ever built for an application. The THF count is a heuristic, an apply spine in a type-role statement, because THF does not separate a type from a term. "Outside the base languages" means a dialect other than cnf, fof, tf0 or th0.

Each — row refines the row above it. The TFF rows are taken over the exact set and do not describe the heuristic's; the heuristic's files are instead divided by dialect, which indicates whether it is identifying types.

A constructor applied at arity ≥ 2 over a type variable is the one shape an elaborator cannot monomorphise into a fresh sort: list($i) is a sort, fun(A, B) is a constructor that has to enter type unification. It is counted for a variable as a direct argument and again for a variable anywhere beneath one, since fun(list(A), $i) is no more monomorphisable than fun(A, B).

Regenerate with mix tptp.census; mix tptp.census --check fails if the results below have gone stale against the library on this machine.

Results

Constructors (TFF)

From the exact TFF walk alone. record_thf/3 sets a boolean and never populates constructors, so the files the THF heuristic found contribute no names, no arities and no domains here — this is a census of the constructors TFF spells unambiguously, not of the library's constructors. Var counts the files where the constructor took a type variable as a direct argument at arity ≥ 2, Var nested where one appeared anywhere beneath an argument.

Provenance

This run