vikraman / 2DTypes

Collaborative work on reversible computing
17 stars 1 forks source link

Fix the example with f, g and h #129

Closed inexxt closed 3 years ago

inexxt commented 3 years ago

Fix the example.

l. 215: What is h here, and how is g related to f?
Given an arbitrary function f : 𝔹 → 𝔹, Toffoli defines a reversible version g : 𝔹 × 𝔹 → 𝔹 × 𝔹 as follows:

 g(r,h) = (r, f(r) ⊕ h)
The reversible function takes an additional "heap" argument and produce an additional "garbage" output. We have:

 g(r,0) = (r, f(r) ⊕ 0) = (r, f(r))
So fixing the first argument to 0 and ignoring the first output we recover f. This construction is used to define the reversible version of modular exponentiation. See the explicit calculation in Examples/ExpMod.agda.
sabry commented 3 years ago

Done. Pushed the revised version of Sec. 2