Look no further: Unification of higher-order patterns in a simply typed lambda-calculus with finite products and terminal type
Roland Fettig und Bernd Löchner http://www.springerlink.com/content/f5q267h680201388/ AFAIK, it has never received much attention, which is a pity. Tobias Am 24/02/2011 17:47, schrieb Rob Arthan: > 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 ------------------------------------------------------------------------------ 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
