proofpeer / proofpeer-proofscript

The language of ProofPeer: ProofScript
MIT License
8 stars 0 forks source link

Implement Term Pattern Matching #9

Closed phlegmaticprogrammer closed 10 years ago

phlegmaticprogrammer commented 10 years ago

I will use higher-order patterns for this (the Dale Miller ones). Had a short email exchange with Colin Sterling about whether higher-order matching in general is practical. Here is his two cents about that:

"Unfortunately higher-order matching has a non-elementary complexity lower bound in the general case. My decision procedure is purely theoretical (if there is a match then there is a bounded size match where the bounds are determined by the problem size). Hence why it is standard to use Miller's simplified matching."

pikan commented 10 years ago

On 2 June 2014 18:00, Steven Obua notifications@github.com wrote:

I will use higher-order patterns for this (the Dale Miller ones). Had a short email exchange with Colin Sterling about whether higher-order matching in general is practical.

As suspected then (regarding Colin's algorithm).

There could be other ideas of Miller (and of others, who've worked on LambdaProlog, for instance) that come in handy in the context of "programming with higher order logic" i.e. when dealing with pragmatic rather than purely theoretical situations.