This page gathers the system-level story: how TensorLang uses explicit tensor programs for fixture-backed world-model demos, trainable fragments, foundation-model scaffolding, v2.0 production capability surfaces, executable relational backends, and dynamical systems.
TensorLang v1.3 uses deterministic fixtures to exercise practical bounded-world tasks: software-system trace prediction, service-span diagnosis, sensor trajectory prediction, and semantic-memory link scoring.
Semantic trace JSONL becomes root-cause examples with event, component, operation, status, reason, duration, and evidence-path features.
Span fixtures normalize into the same trace-world schema for public microservice-style failure classification.
C-MAPSS-style cycle rows train a tiny remaining-useful-life predictor over operating settings and sensor readings.
FB15k-237-style triples score missing relationship hypotheses without asserting them as facts.
tl dataset-list tl dataset prepare semantic-traces --out build/datasets/semantic-traces tl dataset prepare opentel-demo-traces --out build/datasets/opentel tl dataset prepare cmapss --out build/datasets/cmapss tl dataset prepare fb15k237 --out build/datasets/fb15k237 tl benchmark trace-world-fixture --json tl benchmark trace-world-opentel --json tl benchmark cmapss-reservoir-rul --json tl benchmark fb15k237-link-prediction --json
TensorLang supports structured trainable models and small generic numeric training. v1.7 adds generic train-loss graph inspection with finite-difference gradient reference summaries; v1.8 adds bounded research artifacts around the tiny transformer, accelerator plans, optimizer-state manifests, and finite proof-calculus reports.
Train entity/relation embeddings, predict plausible missing facts, and emit scores that can later feed evidence-bearing claims.
Train on structured trace fields including event, component, operation, reason, expected/actual mismatch, status, and duration bucket.
Keep recurrent dynamics fixed, train a small readout, and use the learned readout for deterministic signal or anomaly tasks.
Save/load JSON artifacts with parameter tensors, semantic hash, reproducible seed, backend, and training metrics.
Lower small numeric train losses into inspectable graphs with finite-difference gradient reference summaries.
Training TensorLang models produces predictions, scores, or evidence, not formal proof. Formal verification remains limited to finite Boolean fragments and external proof artifacts.
tl train examples/26_kg_link_prediction_train.tl fit \ --backend auto \ --save-artifact build/kg_model.tla.json \ --json tl eval-model examples/26_kg_link_prediction_train.tl \ --artifact build/kg_model.tla.json \ --json tl lower-autodiff examples/26_kg_link_prediction_train.tl fit \ --backend auto \ --json tl lower-autodiff examples/17_training_linear_regression.tl fit \ --backend auto \ --json tl benchmark kg-training --json tl benchmark autodiff-kg-training --json
TensorLang now has a bounded foundation workflow: tiny MLP or tiny single-head transformer-block character models, reusable artifacts, sharded checkpoint manifests, generation, production-size pretraining plans, local multi-process training, finite proof certificates, and energy-measurement hooks.
Character vocabulary construction with deterministic encode/decode for local text corpora.
Fixed context windows create next-token training examples without network access or external services.
Token embeddings, positional embeddings, an MLP or tiny single-head transformer block, and softmax cross-entropy run in NumPy.
Foundation JSON artifacts store tokenizer, config, learned parameters, loss history, perplexity, and parameter count.
Autoregressive generation loads the artifact and produces deterministic or temperature-sampled text.
The shipped tiny transformer trains with manual reverse-mode; v2.0 adds production pretraining manifests and local multi-process training.
tl foundation-train \ --text "tensorlang trains local language models. tensorlang generates tokens." \ --steps 80 \ --context 8 \ --save-artifact build/foundation.tlf.json \ --json tl foundation-generate \ --artifact build/foundation.tlf.json \ --prompt tensorlang \ --tokens 32 \ --json tl benchmark foundation-lm --json
The executable foundation models are intentionally small enough for local deterministic tests. They prove workflow shapes that larger TensorLang models need: tokenizer, causal examples, train loop, transformer-style block execution, artifact, sharded checkpoint manifest, metrics, generation, production pretraining plan metadata, and local worker-process gradient averaging. They do not claim frontier quality, GPU kernels, or measured energy savings without a baseline.
The old production-research card is now implemented as scoped reference surfaces: production transformer pretraining plans, an executable NumPy accelerator runtime, local multi-process foundation training, and a TensorLang theorem-prover entry point.
tl foundation-pretrain-plan \ --layers 24 \ --heads 16 \ --model-dim 2048 \ --ff-dim 8192 \ --training-tokens 10000000000 \ --tensor-parallel 2 \ --data-parallel 4 \ --out build/pretrain.plan.json \ --json tl run-accelerator \ examples/17_training_linear_regression.tl \ mse \ --target numpy tl foundation-distributed-train \ --text "tensorlang synchronizes gradients." \ --architecture transformer \ --workers 2 \ --steps 4 \ --save-artifact build/foundation.distributed.json \ --json tl theorem-prove \ examples/43_theorem_prover_family.tl
Production-size decoder-transformer manifests include parameter counts, token/step estimates, memory, checkpoint, and parallelism metadata without allocating the full model.
Supported lowered expression graphs execute through the dependency-free NumPy runtime and return actual tensor data plus runtime metadata.
Local worker processes shard next-token examples, compute gradients, synchronize by averaging, and emit normal foundation artifacts.
TensorLang property obligations get proof-search reports with finite-domain rule traces, optional SMT backend use, and unsupported-fragment diagnostics.
TensorLang v1.1 turns relational plans into executable paths. v1.5 feeds the same relational-algebra path with explicit named-axis join/project expressions. v1.6 adds Datalog and TypeDB/TypeQL-style exports. v1.7 broadens train-loss graph inspection for generic numeric training. v1.8 adds accelerator lowering artifacts for supported expression graphs.
Executes supported finite Bool relation plans as deterministic sets of labelled rows.
Uses Python stdlib sqlite3 as a reference backend with executable joins, projections, unions, and fixed-point insertion.
Compares reference evaluator rows against in-memory and SQLite output for supported relation programs.
Emits deterministic Datalog and TypeDB/TypeQL-style text artifacts for supported finite Bool relational plans.
Reports structured JAX-oriented graphs and generic train-loss graphs with finite-difference gradient reference metadata.
Emits deterministic target-labelled graph artifacts for supported expression graphs without claiming executable kernels.
tl backend-list --json tl rel-run examples/29_rel_backend_policy.tl can_do \ --backend inmem \ --json tl rel-run examples/29_rel_backend_policy.tl can_do \ --backend sqlite \ --json tl rel-compare examples/30_rel_backend_reachability.tl reachable \ --backends reference,inmem,sqlite \ --json tl emit-sql examples/29_rel_backend_policy.tl can_do tl emit-datalog examples/29_rel_backend_policy.tl can_do tl emit-typedb examples/29_rel_backend_policy.tl can_do tl lower-relalg examples/32_tensor_logic_primitives.tl user_role_action tl lower-autodiff examples/26_kg_link_prediction_train.tl fit \ --backend auto \ --json tl lower-autodiff examples/17_training_linear_regression.tl fit \ --backend auto \ --json tl lower-accelerator examples/17_training_linear_regression.tl mse \ --target gpu
A system declares state tensors, transition equations, and a simulation mode. Discrete-time steps and Euler integration for continuous-time are supported today, with reservoir-style recurrent examples included.
(module examples.dynamics (tensorlang "1.5") (domain State (size 2) (labels "r0" "r1")) (domain Input (size 1) (labels "u0")) (system TinyReservoir (time continuous (dt 0.1) (steps 3)) (state x (type F64) (shape State) (init (data 0.1 -0.1))) (input u (type F64) (shape Input) (data 1.0)) (param W (type F64) (shape State State) (data (row 0.0 1.0) (row -1.0 0.0))) (dynamics (= dx/dt (tanh (+ (einsum "ij,j->i" W x) u))))))