Random vectors and fast reduction of lambda calculus terms

Em-convex is a lambda calculus, so it could be implemented in Haskell say.

What would be really interesting is the following:

Problem: given two terms A, B, is it true that A, B reduce to the same term C?

Numerical solution:

  • generate a list of 1024 or 2048 dimensional random vectors, before the reduction to happen, to be used later, they will be constants of type E, and a list of random scalars of type N
  •  input two em-convex term, A, B, they are functions over some power of E and N
  •  evaluate A, B and check if A(x)=B(x) for a single argument x, where x is built from the list of random elements:E and random elements:N

How fast is this?


Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )


Connecting to %s