Can anyone give me any pointers to extensions of the Miller/Nipkow algorithms
for higher-order unification and matching for linear patterns to work modulo
pairing and projection? I.e., if I am doing matching, I want `p(x, y)` to be a
valid pattern and I want `\z.(FST z, SND z)` to be an instance of `\(x, y).p(y,
x)` under the substitution [`\(x, y).(y, x)` / `p`].
Regards,
Rob.
------------------------------------------------------------------------------
Free Software Download: Index, Search & Analyze Logs and other IT data in
Real-Time with Splunk. Collect, index and harness all the fast moving IT data
generated by your applications, servers and devices whether physical, virtual
or in the cloud. Deliver compliance at lower cost and gain new business
insights. http://p.sf.net/sfu/splunk-dev2dev
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
