Decidable medical machines, from formulas to Tau

Prerequisites: Tutorial 3 for Tau syntax, Tutorial 6 for MPRD, and Tutorial 22 for the broader medical MPRD context.

This tutorial starts with the small machines that appear inside many medical and wellness programs.

Rather than automating medicine at scale, it shows how a bounded workflow appears in several equivalent forms:

• as a math function,
• as a decision tree,
• as a finite-state machine,
• as ordinary code,
• and as a Tau specification.

These representations are complementary, different lenses on the same computational object.

Part I: what makes a small medical program decidable

The simplest software object in this tutorial is a total function:

It takes an input from X and always returns an output in Y.

If the output is a yes or no verdict, the function becomes a decision procedure:

A predicate P is decidable exactly when some total Boolean program decides it:

That is the mathematical view.

The same object can also be drawn as a finite-state machine:

with:

• Q, a finite set of states,
• Σ, the input alphabet,
• δ, the transition rule,
• q0, the start state,
• F, the set of final states.

For the bounded workflows in this tutorial, decidability means:

Every input reaches a final state, with no loops and no unresolved cases.

By this definition, both calculators and guideline trees qualify as decidable machines.

Part II: one object, four lenses

For the kinds of examples used here, each system can be read in four ways.

First, as composition:

Second, as a decision tree:

• collect bounded facts,
• test one condition,
• branch,
• reach an action leaf.

Third, as a finite-state machine:

Fourth, as logic:

The rest of the tutorial demonstrates each correspondence with concrete examples.

Part III: example A, the max-calorie-deficit calculator

The first example is the user’s own calculator:

• public repo: TheDarkLightX/MaxCaloricDeficitCalc

The motivating problem is simple. A person wants a bounded estimate of the largest calorie deficit that still stays inside a particular published formula.

The math view

Let:

• w = body weight in pounds,
• b = body-fat fraction, so 20% is 0.20,
• f = fat mass in pounds,
• m = maximum deficit in kcal/day.

Then the formulas are:

So the composed function is:

If the program displays an integer result, the bounded calculator can be written as:

The logic view

The arithmetic claim can be written as a relation:

If a program claims some output m, the checker question is:

CorrectClaim is a decidable predicate.

The decision-tree view

Even a calculator has a tiny decision tree:

1. Are the inputs present?
2. Are the inputs in range?
3. If yes, compute the result.
4. If no, reject or escalate.

That becomes:

The finite-state-machine view

The core formula is a single expression, but the user-facing program is a state machine:

This separation of concerns shapes the design.

The mathematical object is:

The interface object is:

with several named phases.

The ordinary-code view

In ordinary code, the cleaned core is small:

double fat_mass_lb = bodyweight_lb * bodyfat_fraction;
int max_deficit_kcal = static_cast<int>(std::floor(31.4 * fat_mass_lb));

The same computation appears in spreadsheet form:

This example reveals a fundamental principle: program synthesis in a spreadsheet, C++, Python, or Tau can preserve the same shape.

The Tau view

The Tau file for this calculator is:

• medical_max_calorie_deficit_formula_v1.tau

The spec is a checker, not a calculator. It takes three inputs, including a claimed result, and outputs whether that claim matches the floor of the formula. The host or user supplies the claim; Tau validates it.

Because the public teaching lane uses bounded integers, the formula is checked in scaled exact arithmetic.

Body fat is encoded in basis points, so 20.00% becomes 2000. Then:

To express the floor relation without floating point, the Tau checker uses:

That is why this example is especially good for Tau. The arithmetic is exact, finite, and integer-only, with no floating-point approximation.

The stream mapping is:

The core always clause:

always
  (((o2[t]:bv[8] = { #x01 }:bv[8]) <->
     ((i1[t]:bv[32] <= { #x000001F4 }:bv[32]) &&
      (i2[t]:bv[32] <= { #x00002710 }:bv[32]) &&
      (i3[t]:bv[32] <= { #x00004E20 }:bv[32])))) &&
  (((o1[t]:bv[8] = { #x01 }:bv[8]) <->
     ((o2[t]:bv[8] = { #x01 }:bv[8]) &&
      (({ #x000186A0 }:bv[32] * i3[t]:bv[32]) <=
       (({ #x0000013A }:bv[32] * i1[t]:bv[32]) * i2[t]:bv[32])) &&
      ((({ #x0000013A }:bv[32] * i1[t]:bv[32]) * i2[t]:bv[32]) <
       ({ #x000186A0 }:bv[32] * (i3[t]:bv[32] + { #x00000001 }:bv[32])))))) &&
  (((o1[t]:bv[8] = { #x00 }:bv[8]) || (o1[t]:bv[8] = { #x01 }:bv[8])) &&
   ((o2[t]:bv[8] = { #x00 }:bv[8]) || (o2[t]:bv[8] = { #x01 }:bv[8]))).

Reading guide:

1. The o2 biconditional is the range check. The hex constants decode as: #x1F4 = 500, #x2710 = 10000, #x4E20 = 20000.
2. The o1 biconditional is the floor relation. #x186A0 = 100000, #x13A = 314. It checks 100000 · m_claim ≤ 314 · w · b_bps < 100000 · (m_claim + 1).
3. The final two disjunctions restrict both outputs to 0 or 1.

Input:  weight = 180 lb, bodyfat = 2000 bps (20%)
Solve:  100000 * o1 <= 314 * 180 * 2000 < 100000 * (o1 + 1)
Output: o1 = 1130 kcal/day

Part IV: example B, kidney function to bounded follow-up

The second example is closer to ordinary medicine.

A patient gets a serum creatinine result, for example 1.1 mg/dL. That result is not yet the same thing as a follow-up decision. A machine still has to:

1. compute eGFR,
2. classify the result,
3. choose a bounded action class.

The official calculator step

The 2021 CKD-EPI creatinine equation (NIDDK, race-free variant, reviewed May 2025) is:

with:

• κ = 0.7 for females or 0.9 for males,
• α = -0.241 for females or -0.302 for males,
• SCr = serum creatinine in mg/dL.

Source:

• NIDDK adult eGFR equations

Creatinine alone is not enough: the equation depends on age and sex, so the host must supply all three.

A concrete worked example

Assumption K1: adult female, age 55, serum creatinine 1.1 mg/dL, using the NIDDK adult 2021 CKD-EPI creatinine equation.

For females, κ = 0.7 and α = -0.241.

Since SCr/κ > 1:

Assembling the equation with the female multiplier 1.012:

This step converts serum creatinine into eGFR, the essential computation:

The National Kidney Foundation’s patient-facing guidance also states that an eGFR below 60 for three months or more, or an eGFR above 60 with kidney damage, can indicate chronic kidney disease. Urine albumin context also matters.

Source:

• NKF eGFR overview

That is why a real deployment needs more than one lab value and one threshold.

The educational follow-up policy

Because full clinical policy is complex, the teaching example uses a simplified decision tree with three action classes:

• watch
• repeat_lab
• human_review

The host computes the exact eGFR. Then it reduces the result to a bounded flag:

Now the policy can be written:

Though simplified for teaching, the pipeline structure mirrors real workflows:

The finite-state-machine view

The kidney lane is a longer but still finite machine:

If data are missing or stale, the machine moves to the human-review branch rather than proceeding with incomplete information.

The decision-tree view

The kidney follow-up gate has the same shape as a small decision tree:

1. Is the result complete and fresh?
2. Is there a red flag?
3. Is eGFR below 60?

The leaves are:

Here b_bps means body-fat percentage encoded in basis points, a_watch means observe, a_repeat means repeat the lab, and a_review means route to human review.

Every input combination reaches exactly one leaf.

The ordinary-code view

The same decision tree in ordinary code:

double egfr = ckd_epi_2021(scr, age, sex);
bool below60 = egfr < 60.0;
if (red_flag || !complete || !fresh) return HUMAN_REVIEW;
if (below60) return REPEAT_LAB;
return WATCH;

The code, the state machine, and the logic formulas all model the same decision process.

The Tau view

The public Tau file is:

• medical_egfr_followup_gate_v1.tau

This file does not recompute the official floating-point equation.

Instead it follows the safer MPRD split:

This split clarifies the architectural boundary between computation and validation.

• some bounded arithmetic objects fit fully inside Tau,
• some official equations are better handled by host computation plus Tau validation.

The Tau spec implements this split with the following stream mapping:

The core always clause:

always
  (o2[t]:bv[8] =
    (i3[t]:bv[8] |
     ({ #x01 }:bv[8] - i1[t]:bv[8]) |
     ({ #x01 }:bv[8] - i2[t]:bv[8]))) &&
  (o1[t]:bv[8] =
    ((i8[t]:bv[8] *
      i5[t]:bv[8] *
      ({ #x01 }:bv[8] - i6[t]:bv[8]) *
      ({ #x01 }:bv[8] - i7[t]:bv[8]) *
      i1[t]:bv[8] *
      i2[t]:bv[8] *
      ({ #x01 }:bv[8] - i3[t]:bv[8]) *
      ({ #x01 }:bv[8] - i4[t]:bv[8])) +
     (i8[t]:bv[8] *
      ({ #x01 }:bv[8] - i5[t]:bv[8]) *
      i6[t]:bv[8] *
      ({ #x01 }:bv[8] - i7[t]:bv[8]) *
      i1[t]:bv[8] *
      i2[t]:bv[8] *
      ({ #x01 }:bv[8] - i3[t]:bv[8]) *
      i4[t]:bv[8]) +
     (i8[t]:bv[8] *
      ({ #x01 }:bv[8] - i5[t]:bv[8]) *
      ({ #x01 }:bv[8] - i6[t]:bv[8]) *
      i7[t]:bv[8] *
      o2[t]:bv[8]))).

Reading guide:

1. The first conjunct computes o2 = human_review_required as the bitwise OR of red_flag, NOT complete (1 - i1), and NOT fresh (1 - i2).
2. The second conjunct computes o1 as the sum of three mutually exclusive products, one for each action class: watch, repeat_lab, and human_review. Because inputs are restricted to 0 or 1, multiplication is conjunction and addition is disjunction over non-overlapping branches.
3. The watch product includes (1 - i4), so it goes to zero whenever eGFR is below 60. The repeat_lab product includes i4, so it only fires when eGFR is below 60. The human_review product fires only when o2 = 1.

Part V: why these examples matter

The two examples above already show four recurring shapes. Tutorial 22 develops the full taxonomy; here is the short version with local pointers.

• Calculator: f : X → Y, local example: max calorie deficit
• Calculator + classifier: g(f(x)) ∈ K, local example: creatinine → eGFR → below_60 band
• Classifier + gate: Allow(a,s) ⇔ P1(s) ∧ ... ∧ Pn(s), local example: watch / repeat_lab / human_review
• Temporal gate: Fresh(x,t) ⇔ t - time(x) ≤ Δ, local example: stale lab → human_review

The same shapes appear across many medical workflows: potassium follow-up trees, HbA1c monitoring and retest windows, CBC or anemia follow-up routing, and refill authorization under explicit freshness and identity rules.

They differ medically but share a common software architecture.

Part VI: why decidability matters in medicine and wellness software

For a bounded workflow, decidability is not theoretical, it is a practical necessity. It guarantees that every input reaches a final decision without looping indefinitely.

The totality claim is:

For a finite-state machine:

For a gate:

The practical meanings are:

• every bounded case reaches an explicit conclusion,
• every out-of-scope case routes to a known fallback,
• and the entire decision surface is auditable.

That is why simple medical programs are such good teaching objects.

Part VII: where Tau fits, and where it should stop

Tau is strongest when the object is:

• bounded,
• typed,
• integer-scaled or Boolean,
• and naturally expressed as invariants or action gates.

That makes the calorie example (Shape 1 in Part V: a pure calculator) a direct Tau object.

The kidney example shows the other lane. Shape 2+3 from Part V (calculator followed by classifier followed by gate) is too rich for a single Tau spec because the official eGFR equation uses floating-point exponentiation. The architectural split is:

This is the same split used in MPRD:

• host code handles the rich arithmetic or parsing,
• Tau validates the bounded decision shape,
• execution only happens through the checked action class.

Tau should not be used for:

• open-ended reasoning or unconstrained search,
• floating-point computation that requires exact numeric fidelity,
• unbounded state spaces where totality cannot be guaranteed,
• or tasks where the action menu is not sharply defined.

Those belong on the host side or in a different tool altogether.

The layers above remain grounded in decidable machines, not hidden complexity. It is just bounded medical machines composed inside a stricter architecture.

Part VIII: downloadable specs and trace evidence

Spec files:

• medical_max_calorie_deficit_formula_v1.tau (checker)
• medical_max_calorie_deficit_calculator_v1.tau (direct calculator)
• medical_egfr_followup_gate_v1.tau

Replay artifacts:

• medical_decidable_tau_traces.json
• generate_medical_decidable_tau_artifacts.py

Companion lab:

• medical_decidable_machines_lab.html

That means a reader can inspect:

• the formulas,
• the Tau specs,
• the replayable traces,
• and the host-side interactive demo.

Calorie trace walkthrough

Two cases from the recorded traces show the floor check in action:

For the exact match:

Both inequalities hold, so o1 = 1.

For the bad claim:

The lower bound fails, so o1 = 0. The range check still passes (o2 = 1) because all three inputs are within bounds.

Kidney trace walkthrough

Two cases show how the gate blocks a wrong action class and allows the right one:

In the bad_watch case, the model proposes watch even though eGFR is below 60. The watch branch of the Tau spec has the factor 1 - i4:

That zero kills the entire watch product, so o1 = 0. The gate denies the action.

In the repeat_ok case, the model instead proposes repeat_lab. The repeat branch has the factor i4:

All other factors in the repeat product are also 1, so o1 = 1. The gate allows the action.

Part IX: interactive lab

Part X: what to take away

Small medical software need not begin with opaque reasoning algorithms.

It can begin with tiny, decidable machines:

• calculators,
• classifiers,
• gates,
• temporal freshness checks,
• and explicit escalation paths.

Once those machines are visible, the same object can be seen as:

• a formula,
• a decision tree,
• a finite-state machine,
• ordinary code,
• a spreadsheet,
• or a Tau specification.

That is the main lesson.

Every object in this tutorial satisfies the totality property from Part I:

The calorie calculator is a total function: every bounded input reaches a floor result or an out-of-range error. The kidney policy is a finite decision tree over a bounded flag surface: every fact pattern designates one admissible class, and a wrong proposal is denied rather than silently executed. In both cases, every input reaches a definite outcome, with no loops and no unresolved states. That is decidability in practice.

The code may change. The notation may change. The shape does not have to change.

The next layer up composes these decidable machines inside the MPRD architecture from Tutorial 22.