Untrusted Authors, Trusted Answers: A Calculus of Fidelity-Graded Translations

תקציר מקורי באנגליתarXiv:2607.14137v2 Announce Type: cross Abstract: To answer a question about a program, move the program to where the question is decidable. Every such move is a translation, and every translation is a place to be wrong. We study translation as a graph -- many languages, a few reasoning targets, independently built routes of honestly different trustworthiness -- and give it a calculus: pairs of languages close commuting squares that are directional (exactness is the identity-embedding special case of over-approximation), checkable per program, and composable, a route's contract being the componentwise meet of its hops' contracts -- assurance class, direction, kept observables, measured cost. One asymmetry organizes trust: witness-carrying answers are self-certifying by replay at the source