4 Formální překlady

Formální překlad \(Z\) definujeme jako binární relaci mezi formálními jazyky \(L\) a \(V\):

\[ Z \subseteq L \times V \]

Formální překlad tak přiřazuje řetězcům z jazyka \(L\) (definiční obor) řetězce (překlady) z jazyka \(V\) (obor hodnot).

Jednoznačný formální překlad je formální překlad, který je zároveň funkcí (může být i parciální).

Tedy pro každý prvek z definičního oboru tak existuje jeden prvek z oboru hodnot (či nejvýše jeden v případě parciální funkce).