Created
February 29, 2012 23:47
-
-
Save sandello/1945566 to your computer and use it in GitHub Desktop.
Seemingly Impossible Functional Program in C++
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
// Ivan Pouzyrevsky, EWSCS'12. | |
#include <iostream> | |
#include <functional> | |
#include <memory> | |
#include <utility> | |
// This is a C++ implementation for Seemingly Impossible Functional Program, which in finite time tests whether | |
// a computable predicate on binary strings yields True for some binary string. It does so by exhaustive search | |
// on whole space. Some nasty-nasty tricks like call-by-need can make this algorithm run fast. | |
// | |
// To compile this program you have to have a decent C++11 compiler (i. e. g++-4.5+). You can check for C++11 | |
// support for your compiler at http://wiki.apache.org/stdcxx/C%2B%2B0xCompilerSupport. | |
// | |
// Observe & have fun. | |
// | |
// For more references see: | |
// - http://www.cs.bham.ac.uk/~mhe/.talks/EWSCS2012/ | |
// - http://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/ | |
//////////////////////////////////////////////////////////////////////////////// | |
// Abstractions for lazy evaluations. | |
// A value of type T is obtained by evaluating the given closure on-demand. | |
template <class T> | |
class LazyEvaluation | |
{ | |
public: | |
explicit LazyEvaluation(T value) | |
: value_(new T(std::move(value))), closure_() | |
{ } | |
explicit LazyEvaluation(std::function< T(void) > closure) | |
: value_(), closure_(std::move(closure)) | |
{ } | |
LazyEvaluation(const LazyEvaluation& other) | |
: value_(other.value_) | |
, closure_(other.closure_) | |
{ } | |
LazyEvaluation(LazyEvaluation&& other) | |
: value_(std::move(other.value_)) | |
, closure_(std::move(other.closure_)) | |
{ } | |
std::shared_ptr<T> Get() const | |
{ | |
if (!value_) { | |
value_.reset(new T(closure_())); | |
} | |
return value_; | |
} | |
private: | |
mutable std::shared_ptr<T> value_; | |
std::function< T(void) > closure_; | |
}; | |
// A copyable lazily evaluated value. | |
template <class T> | |
class Lazy | |
{ | |
public: | |
template <class U> | |
explicit Lazy(U&& x) | |
: impl_(new LazyEvaluation<T>(std::forward<U>(x))) | |
{ } | |
Lazy(Lazy& other) | |
: impl_(other.impl_) | |
{ } | |
Lazy(const Lazy& other) | |
: impl_(other.impl_) | |
{ } | |
Lazy(Lazy&& other) | |
: impl_(std::move(other.impl_)) | |
{ } | |
std::shared_ptr<T> Get() const | |
{ | |
return impl_->Get(); | |
} | |
private: | |
std::shared_ptr< LazyEvaluation<T> > impl_; | |
}; | |
//////////////////////////////////////////////////////////////////////////////// | |
// The EVAL() method forces the evaluation of an expression. | |
template <class T> | |
struct EvaluationTraits | |
{ | |
typedef const T& R; | |
static R Evaluate(const T& x) { return x; } | |
}; | |
template <class T> | |
struct EvaluationTraits< Lazy<T> > | |
{ | |
typedef const T& R; | |
static R Evaluate(const Lazy<T>& x) { return *(x.Get()); } | |
}; | |
template <class T> | |
typename EvaluationTraits<T>::R EVAL(const T& x) | |
{ | |
return EvaluationTraits<T>::Evaluate(x); | |
} | |
//////////////////////////////////////////////////////////////////////////////// | |
// A lazily evaluated binary sequence. | |
enum class Bit | |
{ | |
Zero, | |
One | |
}; | |
struct BitSequence | |
{ | |
Lazy<Bit> Value; | |
Lazy<BitSequence> Next; | |
BitSequence(const BitSequence& other) | |
: Value(other.Value) | |
, Next(other.Next) | |
{ } | |
BitSequence(BitSequence&& other) | |
: Value(std::move(other.Value)) | |
, Next(std::move(other.Next)) | |
{ } | |
template <class A1, class A2> | |
BitSequence(A1&& a1, A2&& a2) | |
: Value(std::forward<A1>(a1)), Next(std::forward<A2>(a2)) | |
{ } | |
}; | |
//////////////////////////////////////////////////////////////////////////////// | |
// The most important types in this program. | |
typedef std::function< bool(Lazy<BitSequence>) > Predicate; | |
Lazy<BitSequence> Find(Predicate); | |
bool ForSome(Predicate); | |
bool ForEvery(Predicate); | |
//////////////////////////////////////////////////////////////////////////////// | |
// The implementations. | |
Lazy<BitSequence> Find(Predicate p) | |
{ | |
Predicate p0 = [=] (Lazy<BitSequence> seq) -> bool { | |
return p(Lazy<BitSequence>([=] () { | |
return BitSequence(Bit::Zero, seq); | |
})); | |
}; | |
Predicate p1 = [=] (Lazy<BitSequence> seq) -> bool { | |
return p(Lazy<BitSequence>([=] () { | |
return BitSequence(Bit::One, seq); | |
})); | |
}; | |
return Lazy<BitSequence>([=] () { | |
// This optimization reduces time from exponential to linear. | |
// Try to guess why. :7 | |
auto temporary = Find(p0); | |
if (p0(temporary)) { | |
return BitSequence(Bit::Zero, temporary); | |
} else { | |
return BitSequence(Bit::One, Find(p1)); | |
} | |
}); | |
} | |
bool ForSome(Predicate p) | |
{ | |
return p(Find(p)); | |
} | |
bool ForEvery(Predicate p) | |
{ | |
return !ForSome([=] (Lazy<BitSequence> seq) -> bool { return !p(seq); }); | |
} | |
//////////////////////////////////////////////////////////////////////////////// | |
bool AreEqual( | |
std::function< int(Lazy<BitSequence>) > f, | |
std::function< int(Lazy<BitSequence>) > g) | |
{ | |
return ForEvery([=] (Lazy<BitSequence> seq) -> bool { return f(seq) == g(seq); }); | |
} | |
//////////////////////////////////////////////////////////////////////////////// | |
// Auxiliary code to print stuff. | |
std::ostream& operator<<(std::ostream&os, Bit x) | |
{ | |
return os << ((x == Bit::Zero) ? "0" : "1"); | |
} | |
void Dump(Lazy<BitSequence> seq, int depthLimit, int currentDepth = 0) | |
{ | |
if (currentDepth >= depthLimit) { | |
return; | |
} | |
std::cout << EVAL(EVAL(seq).Value); | |
Dump(EVAL(seq).Next, depthLimit, currentDepth + 1); | |
if (currentDepth == 0) { | |
std::cout << "..." << std::endl; | |
} | |
} | |
//////////////////////////////////////////////////////////////////////////////// | |
// Running example. | |
#define N(z) EVAL(z).Next | |
#define V(z) EVAL(z).Value | |
#define E(z) EVAL(z) | |
#define Z(z) static_cast<int>(EVAL(z)) | |
static int SimplePredicateCallCount = 0; | |
bool SimplePredicate(Lazy<BitSequence> seq) | |
{ | |
++SimplePredicateCallCount; | |
return E(V(N(N(seq)))) == Bit::One; // Tests third bit of the sequence. | |
} | |
// F == G, F != H | |
int MyF(Lazy<BitSequence> seq) | |
{ | |
return 17 * Z(V(seq)) + 42 * Z(V(N(seq))) + 239 * Z(V(N(N(N(seq))))); | |
} | |
int MyG(Lazy<BitSequence> seq) | |
{ | |
return 17 * Z(V(seq)) + 42 * Z(V(N(seq))) + 239 * Z(V(N(N(N(seq))))); | |
} | |
int MyH(Lazy<BitSequence> seq) | |
{ | |
return 42 * Z(V(seq)) + 17 * Z(V(N(seq))) + 239 * Z(V(N(N(N(seq))))); | |
} | |
#undef Z | |
#undef E | |
#undef V | |
#undef N | |
//////////////////////////////////////////////////////////////////////////////// | |
int main(int, char**) | |
{ | |
std::cout << "(FORSOME) " << ForSome(&SimplePredicate) << std::endl; | |
std::cout | |
<< "Predicate was invoked " | |
<< SimplePredicateCallCount | |
<< " times." << std::endl; | |
std::cout << "(WITNESS) "; | |
Dump(Find(&SimplePredicate), 8); | |
std::cout << "(MyF == MyG)? " << AreEqual(&MyF, &MyG) << std::endl; | |
std::cout << "(MyF == MyH)? " << AreEqual(&MyF, &MyH) << std::endl; | |
return 0; | |
} | |
/** Original Haskell code is as follows. | |
data Bit = Zero | One deriving (Eq, Show) | |
type Cantor = [ Bit ] | |
find :: (Cantor -> Bool) -> Cantor | |
forsome :: (Cantor -> Bool) -> Bool | |
forevery :: (Cantor -> Bool) -> Bool | |
find p = h : find (\a -> p (h : a)) | |
where h = if forsome (\a -> p (Zero : a)) then Zero else One | |
forsome p = p (find p) | |
forevery p = not (forsome (\a -> not (p a))) | |
equal :: (Cantor -> Integer) -> (Cantor -> Integer) -> Bool | |
equal f g = forevery (\a -> f a == g a) | |
** Now you see why C++ is not-so-good language. | |
** Hope you've enjoyed this gist. | |
**/ |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment