Polynomial-time pairing and unpairing

The pairing codec pair of Complexitylib.Encoding.Pairing is the library's canonical way to hand a machine two strings at once. This file records that the codec is polynomial-time in both directions: pairing two polynomial-time values is polynomial-time, and so are the projections pairFst / pairSnd, whose scanners are the block machines of Cobham's algebra.

Main results

• pairFst_mem_FP, pairSnd_mem_FP — the projections are polynomial-time
• mem_FP_pair — pairing two polynomial-time functions is polynomial-time
• mem_FP_pair_right — pairing a polynomial-time value with the input itself
• mem_P_preimage_pairFst, mem_P_preimage_pairSnd — deciding a language of one component of a pair is polynomial-time

Polynomial-time facts

theorem Complexity.pairFst_mem_FP : pairFst ∈ FP

The first projection is polynomial-time.

theorem Complexity.pairSnd_mem_FP : pairSnd ∈ FP

The second projection is polynomial-time.

theorem Complexity.mem_FP_pair {a b : List Bool → List Bool} (ha : a ∈ FP) (hb : b ∈ FP) : (fun (z : List Bool) => pair (a z) (b z)) ∈ FP

Pairing is polynomial-time: two polynomial-time functions can be evaluated on a common input and paired in polynomial time.

theorem Complexity.mem_FP_pair_right {f : List Bool → List Bool} (hf : f ∈ FP) : (fun (x : List Bool) => pair (f x) x) ∈ FP

Pairing the input on the right of a polynomial-time value is polynomial-time. This is mem_FP_pairWithInput; the mirror image is mem_FP_pair id_mem_FP hf.

theorem Complexity.mem_P_preimage_pairFst {L : Language} (hL : L ∈ P) : pairFst ⁻¹' L ∈ P

A language of the first component of a pair is polynomial-time decidable.

theorem Complexity.mem_P_preimage_pairSnd {L : Language} (hL : L ∈ P) : pairSnd ⁻¹' L ∈ P

A language of the second component of a pair is polynomial-time decidable.