Overview

This post arose out of my attempts to understand IDA and ways it could fail. It might help you do the same and could provide useful vocabulary for discussing desiderata for IDA.

We want IDA to satisfy progress---decomposition should make answering questions easier---and preservation---semantics should be retained across transformations. We need progress in each decomposition and, furthermore, repeated decompositions must be able to eventually simplify each question such that it can be answered directly by a human. Also, each decomposition and aggregation of questions and answers must introduce no more than a bounded amount of semantic drift and, furthermore, repeated decompositions and aggregations should also introduce no more than a bounded amount of semantic drift.

IDA

Iterated distillation and amplification (henceforth IDA) is a proposal for improving the capability of human-machine systems to suprahuman levels in complex domains where even evaluation of system outputs may be beyond unaugmented human capabilities. For a detailed explanation of the mechanics, I'll refer you to the original paper just linked, section 0 of Machine Learning Projects for Iterated Distillation and Amplification, or one of the many other explanations floating around the Web.

We can view IDA as dynamic programming with function approximation^[1] instead of a tabular cache. Just like the cache in dynamic programming, the machine learning component of IDA is a performance optimization. We can excise it and look at just the divide-and-conquer aspect of IDA in our analysis. Then this simplified IDA roughly consists of: (1) repeatedly decomposing tasks into simpler subtasks; (2) eventually completing sufficiently simple subtasks; and (3) aggregating outputs from subtasks into an output which completes the original, undecomposed task. We'll examine this simplified model^[2] in the rest of the post. (If you'd like a more concrete description of the divide-and-conquer component of IDA, there's a runnable Haskell demo here.)

Safety is progress plus preservation

For type systems, the slogan is "safety is progress plus preservation". Because we're using this only as a cute analogy and organizing framework, we'll not get into the details. But for type systems:

Progress: "A well-typed term is [...] either [...] a value or it can take a step according to the evaluation rules."
Preservat

...