{"schema_version":1,"experiment_id":"eoa_inverse_innovation_exp04_retrieval_first_paired20_20260802","cell_id":"computability_boundary_mapping__public_administration_policy","hypothesis_id":"H1","search_queries":["benefits eligibility rule language termination decidable grammar rules as code","policy rules as code restricted language guaranteed termination eligibility","Catala programming language termination recursion totality benefits rules","OpenFisca formula cycle detection recursion termination eligibility","Cedar policy language termination guaranteed evaluation recursion official","Rego policy language termination recursion guaranteed official","DMN FEEL recursion termination decision tables eligibility rules standard","benefits rules engine timeout eligibility denial automation audit"],"sources":[{"source_id":"PA-1","title":"Cedar security","publisher":"Cedar Policy Language","url":"https://docs.cedarpolicy.com/other/security.html","source_class":"OFFICIAL_PRODUCT_DOCUMENTATION","claims_supported":["Cedar policies are guaranteed to terminate, with bounded input sizes recommended for resource safety.","Cedar excludes I/O, provides schema validation, formally models core artifacts in Lean, and differentially tests the production implementation.","This is a close neighboring-domain precedent for an enforceable terminating policy language with pre-use validation."]},{"source_id":"PA-2","title":"Policy validation","publisher":"Cedar Policy Language","url":"https://docs.cedarpolicy.com/policies/validation.html","source_class":"OFFICIAL_PRODUCT_DOCUMENTATION","claims_supported":["Cedar expects policy validation before policies are used for decisions.","Its schema acts as an input contract, and validation soundness has been formally proved, although some runtime errors remain outside the guarantee.","This overlaps strongly with enforceable admission rules and a pre-deployment correctness obligation, but it addresses authorization rather than benefit eligibility."]},{"source_id":"PA-3","title":"rego_recursion_error: rule {name} is recursive","publisher":"Styra","url":"https://docs.styra.com/opa/errors/rego-recursion-error/rule-name-is-recursive","source_class":"COMMERCIAL_FIRST_PARTY","claims_supported":["Rego disallows loops and direct, indirect, or potentially dynamic recursion so policy evaluation can be known to terminate.","The compiler rejects recursive policy dependencies, directly instantiating syntactically enforced language-fragment restriction."]},{"source_id":"PA-4","title":"Catala: A Programming Language for the Law","publisher":"ACM / Catala research team","url":"https://arxiv.org/abs/2103.03198","source_class":"PRIMARY_RESEARCH","claims_supported":["Catala translates statutes into executable programs and was evaluated on French family benefits and US tax law.","Its core compiler transformations were proved correct using F*, and formalization uncovered a bug in an official implementation.","The source does not report a per-rule-set termination certificate or historical-construct retention study."]},{"source_id":"PA-5","title":"Inferences","publisher":"OpenFisca","url":"https://openfisca.readthedocs.io/en/latest/coding-the-legislation/inferences.html","source_class":"OFFICIAL_PRODUCT_DOCUMENTATION","claims_supported":["OpenFisca benefit formulas can use a cycle limit to stop computation into prior periods, leaving some values uncomputed.","OpenFisca warns that inference mechanisms can be inconsistent or unpredictable and documents silent default-value behavior as unsuitable for production expectations.","This supports the practical concern about cycles and misleading fallback values, but not the specific claim that timeouts are coded as ineligibility."]},{"source_id":"PA-6","title":"Variables and formulas","publisher":"OpenFisca","url":"https://openfisca.readthedocs.io/en/latest/key-concepts/variables.html","source_class":"OFFICIAL_PRODUCT_DOCUMENTATION","claims_supported":["OpenFisca represents tax and benefit legislation through executable formula dependencies, including basic-income calculations.","When a value cannot be calculated for a requested period, the engine may return a configured default value, demonstrating a direct benefit-domain analogue for fallback semantics."]},{"source_id":"PA-7","title":"Semantics and Analysis of DMN Decision Tables","publisher":"Calvanese et al.","url":"https://arxiv.org/abs/1603.07466","source_class":"PRIMARY_RESEARCH","claims_supported":["DMN decision tables use a restricted expression form to encode business decisions.","The work defines formal semantics and scalable pre-deployment checks for overlapping and missing rules, providing a neighboring precedent for analyzable restricted rule authoring.","Its demonstrated domain is credit lending, and its checks establish table consistency and completeness rather than general totality plus semantic correctness of benefit legislation."]}],"proximity":"SUBSTANTIAL_COLLISION","closest_analogues":[{"name":"Cedar terminating policy language and formally proved pre-use validation","similarity":"Very high mechanism-level similarity: a bounded policy language guarantees termination, schema admission is mechanically checked before decision use, and validation soundness is formally proved.","remaining_difference":"Cedar governs authorization rather than statutory benefit eligibility and does not report retention of historical benefit-rule constructs or a per-rule semantic-fidelity certificate against legislation.","source_ids":["PA-1","PA-2"]},{"name":"Rego compiler rejection of recursive policy rules","similarity":"Directly matches the proposed causal lever of syntactically excluding constructs that prevent a termination guarantee.","remaining_difference":"The located practice concerns general infrastructure and authorization policy, not benefit-rule translation, legislative correctness witnesses, or applicant-facing denial handling.","source_ids":["PA-3"]},{"name":"Catala verified statutory programming for family benefits","similarity":"Direct workflow and domain overlap: statutes and family-benefit rules are translated into executable programs, with formally verified compiler steps.","remaining_difference":"The source establishes compiler-transformation correctness, not an enforceable total language, a rule-set-level totality-and-semantic-correctness witness, or an 80% construct-retention result.","source_ids":["PA-4"]},{"name":"OpenFisca executable benefit formulas with cycle bounds and defaults","similarity":"Direct benefit-domain overlap and concrete evidence that formula dependencies, cycle bounds, missing computations, and default values require explicit governance.","remaining_difference":"OpenFisca documents operational controls and caveats rather than restricting all authors to a proved-total grammar with mandatory deployment certificates.","source_ids":["PA-5","PA-6"]},{"name":"DMN restricted decision tables with formal completeness and overlap analysis","similarity":"Uses constrained decision-rule notation and performs formal checks before critical business decisions are executed.","remaining_difference":"The checks cover table overlap and missing cases, not termination and statutory semantic correctness, and the evaluated application is lending rather than public benefits.","source_ids":["PA-7"]}],"overlapping_components":["Machine-executable policy-rule authoring","Syntactically enforceable policy-language restrictions","Compiler rejection of recursive or potentially recursive dependencies","Guaranteed terminating policy evaluation","Pre-deployment schema and rule validation","Formally proved validator or compiler properties","Restricted decision-table notation","Formal completeness and overlap analysis","Executable tax-and-benefit formulas","Cycle bounds and fallback/default-value behavior"],"remaining_contrastive_claim":"No located source demonstrates a production public-benefits workflow that mechanically admits only terminating rule sets, requires a rule-set-level totality-and-legislative-correctness certificate before deployment, and retains at least 80% of historically used rule constructs.","claim_falsifier":"A deployed-system specification, evaluation, patent, or primary study showing all three elements in public benefits—mechanically enforced termination, mandatory per-rule-set totality and semantic-correctness certification, and measured retention of at least 80% of historical constructs—would falsify the remaining claim.","problem_support":"MODERATE","recommendation":"RESEARCH","world_novelty_boundary":"The broad intervention is not world-novel: terminating restricted policy languages, compiler-enforced recursion bans, formally proved pre-use validation, verified statutory-language compilation, and analyzable restricted decision tables already exist. The bounded unresolved territory is their combined application to production benefit eligibility with rule-set-level legislative-fidelity certificates and measured construct coverage; this ordinary-web search found no direct deployment evidence or matching patent, but it is not a patent-office-grade novelty determination."}