Module FlatCurry.Typed.NonDet2Det

This module contains a transformation from possibly non-deterministically defined operations into purely deterministic operations. The transformation is based on the "planned choices" approach described in this paper:

S. Antoy, M. Hanus, and S. Libby: Proving non-deterministic computations in Agda. In Proc. of the 24th International Workshop on Functional and (Constraint) Logic Programming (WFLP 2016), volume 234 of Electronic Proceedings in Theoretical Computer Science, pages 180--195. Open Publishing Association, 2017.

Thus, an additional "choice plan" argument is added to each non-deterministic operation. This plan determines the branches chosen by the operation to compute some value.

This transformation can be used to verify non-determinstic operations by showing their correct behavior for all possible plans.

Author: Michael Hanus

Version: September 2019

Summary of exported operations:

nondetOfFuncDecls
                  ::  [AFuncDecl TypeExpr] -> [((String,String),Bool)]

Returns the non-determinism status for all functions in a list of function declarations.

addChoiceFuncDecl
                  ::  [((String,String),Bool)] -> (TypeExpr,(String,String),(String,String),(String,String)) -> AFuncDecl TypeExpr -> AFuncDecl TypeExpr

Add a "choice plan" argument to a function declaration for all non-deterministic functions (according to first argument).

Exported operations:

nondetOfFuncDecls :: [AFuncDecl TypeExpr] -> [((String,String),Bool)]

Returns the non-determinism status for all functions in a list of function declarations. It is assumed that this list contains the declarations of all functions occurring in these declarations. It is implemented by a very simple fixpoint iteration. This is sufficient for the small lists considered in this application.

addChoiceFuncDecl :: [((String,String),Bool)] -> (TypeExpr,(String,String),(String,String),(String,String)) -> AFuncDecl TypeExpr -> AFuncDecl TypeExpr

Add a "choice plan" argument to a function declaration for all non-deterministic functions (according to first argument). The first argument maps qualified function names into a Boolean flag which is true if the function is (or might be) non-deterministic. The second argument is a tuple (cpType,chooseF,lchoiceF,rchoiceF) describing the types and operations implementing the choice plan:

cpType -- the type of the choice plan
chooseF  :: cpType -> Bool   -- the name of the choose operation
lchoiceF :: cpType -> cpType -- the name of the lchoice operation
rchoiceF :: cpType -> cpType -- the name of the lchoice operation

For instance, these types and operations can be implemented as follows in Curry:

data Choice = Plan Bool Choice Choice

choose :: Choice -> Bool
choose (Plan True  _ _) = True
choose (Plan False _ _) = False

lchoice :: Choice -> Choice
lchoice (Plan _ l _) = l

rchoice :: Choice -> Choice
rchoice (Plan _ _ r) = r

As an example, consider the following operations:

insert :: a -> [a] -> [a]
insert x []     = [x]
insert x (y:ys) = x : y: ys ? y : insert x ys

perm :: [a] -> [a]
perm []     = []
perm (x:xs) = insert x (perm xs)

Since both operations are non-deterministic, they are transformed into the following code:

insert :: Choice -> a -> [a] -> [a]
insert _ x []     = [x]
insert c x (y:ys) = if choose c then x : y: ys
                                else y : insert (lchoice c) x ys

perm :: Choice -> [a] -> [a]
perm _ []     = []
perm c (x:xs) = insert (lchoice c) x (perm (rchoice c) xs)