wimmers / poly-reductions

Polynomial-time reductions in Isabelle/HOL
2 stars 13 forks source link

Reduction from IMP- to IMP-- #28

Closed notiho closed 3 years ago

notiho commented 3 years ago

Since the reduction from IMP-- to SAS+ appears not that easy, @mabdula and I think that it makes sense to solve #8 by going the route IMP- -> IMP-- -> SAS+ . This would probably involve something like bit-blasting. The reduction should be given a maximal number of bits for each register, and then simulate IMP- registers with multiple IMP-- registers, each holding a single bit. Then, instructions of the form x ::= y + z that are missing in IMP-- can be replaced by a binary addition (accordingly for subtraction), using only increments and decrements existing in IMP--.

maxhaslbeck commented 3 years ago

closed by merged PR #25