哪些编程语言支持等式重写、可自动生成定律并搜索最优重写？

函数式程序中一类典型的低效问题，是依据规范编写的reverse这类函数：

import Prelude()

[] ++ ys = ys
(x:xs) ++ ys = x:(xs ++ ys)

reverse []     = []
reverse (x:xs) = (reverse xs) ++ [x]

利用结合律，可以推导出reverse的高效实现：

-------- 重写推导过程 ------

-- 规则：由`++`的定义推导出的恒等式
-- reverse xs = reverse xs ++ []

-- 规则：空列表性质，做模式拆分
-- reverse []      = reverse [] ++ []
-- reverse (x::xs) = reverse (x::xs) ++ [] 

-- 规则：套用`reverse`自身的定义
-- reverse []      = []                
-- reverse (x::xs) = (reverse xs ++ [x]) ++ []

-- 规则：再次利用`++`的结合律推导等价形式
-- reverse []      = []                
-- reverse (x::xs) = reverse xs ++ ([x] ++ [])

-- 规则：套用`++`的空列表消解规则
-- reverse []      = []                
-- reverse (x::xs) = reverse xs ++ (x::[])

-- 规则：引入带累加器的辅助函数
-- reverse' []      acc = []                
-- reverse' (x::xs) acc = reverse xs ++ acc
-- reverse  xs = reverse' xs []

reverse_eff xs = reverse' xs []
  where 
    reverse' [] ys  = ys
    reverse' (x:xs) ys  = reverse' xs (x:ys)

这类低效问题的根源最初来自哪里？

• 我们为++指定了特定的执行顺序
• 编程语言定义的组合规则，为++的组合方式限定了固定顺序
• 编程语言无法识别从代码本身推导出的定律，也不具备效率优化的相关概念

我们实际想要实现的需求是：

• 定义一个经过所有相关定律合理商化的（函数式）++关系
• 对该关系使用关系组合，隐藏内部采用的具体括号嵌套方式
• 在调用位置选择最匹配访问模式与目标的括号嵌套方案（对reverse函数而言，这意味着调整所有括号位置，匹配结果列表的构造方式）

是否存在能够自动生成程序相关定律、并可根据指定指标搜索最优重写方案的编程语言？

内容的提问来源于stack exchange，提问作者nicolas