search

wimmers / poly-reductions

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

Refinement of simple problems to IMP- #6

Open wimmers opened 4 years ago

wimmers commented 4 years ago

We need to be able to refine HOL functions to programs in some WHILE language with a cost model (from now referred to as IMP-). This is to give our polynomial-time reductions a meaningful foundation in terms of a computation model.

We can adapt previous work of Max Haslbeck and Peter Lammich:

A good starting point should be any of our existing reductions.

wimmers commented 4 years ago

After adding the additional refinement step from NREST to NREST-, I will add separate issues for these. The issue at hand should be considered for tracking work on a first example (yet to be picked).