search

fritzo / pomagma

An inference engine for extensional untyped λ-calculus
Other
17 stars 2 forks source link

Infer associativity in cartographer/infer #27

Closed fritzo closed 9 years ago

fritzo commented 9 years ago

The following rules do not require full function tables:

// ----------------------------------
// EQUAL APP COMP x y z APP x APP y z
//
// -------------------------------------
// EQUAL COMP COMP x y z COMP x COMP y z
//
// -------------------------------------
// EQUAL JOIN JOIN x y z JOIN x JOIN y z
//
// -------------------------------------
// EQUAL RAND RAND x y z RAND x RAND y z