12
$\begingroup$

Klop, van Oostrom, and de Vrijer have a paper on the lambda calculus with patterns.

http://www.sciencedirect.com/science/article/pii/S0304397508000571

In some sense, a pattern is a tree of variables -- though I am just thinking of it as a nested tuple of variables, for example, ((x,y),z),(t,s)).

In the paper they showed that if the patterns are linear, in the sense that no variable in a pattern is repeated, then the rule

(\p . m) n = m [n/p]

where p is a variable pattern and n is a tuple of terms with the exact same shape as p, is confluent.

I am curious if there are similar developments in the literature for the lambda calculus with patterns and the additional eta rule (expansion, reduction, or just equality).

In particular, by eta, I mean 

m = \lambda p . m p

More directly, I am curious what properties such a lambda calculus would have. For example, is it confluent?

It forces the classifying category to be closed because it forces the property that

m p = n p implies m = n

By using the \xi-rule in between. But perhaps something could go wrong?

Improve this question
$\endgroup$
4
  • $\begingroup$ Can you write put what eta rule you mean? Unless it's very strange you should be able to encode it using sums and make a simulation argument. $\endgroup$
    – Max New
    Commented Aug 30, 2017 at 13:16
  • 2
    $\begingroup$ @MaxNew: it looks like he's asking about the untyped calculus. Everything about patterns works perfectly with types (I oh-so-modestly suggest my own Focusing on Pattern Matching), but untyped lambda calculus is different enough from typed LC (especially wrt eta) that I don't dare to answer without doing the proofs. $\endgroup$
    – Neel Krishnaswami
    Commented Aug 31, 2017 at 10:12
  • $\begingroup$ @MaxNew: What would encoding by sums entail? $\endgroup$
    – Jonathan Gallagher
    Commented Sep 6, 2017 at 3:43
  • $\begingroup$ @NeelKrishnaswami: I am actually interested in both. I think I am nervous about having variables of a product type together with the eta rule. I think this is done, for example, dicosmo.org/Articles/JFP96.pdf. But if I'm mistaken, please correct me. Then you have equalities like \lambda x .m x = m = \lambda (p,q) . m (p,q), for example. Thanks for the link to your paper! $\endgroup$
    – Jonathan Gallagher
    Commented Sep 6, 2017 at 3:48

1 Answer 1

Reset to default
7
$\begingroup$

This is not a complete answer; it is a comment that got too large.

If you extend typed lambda calculus with products with projective eliminators (ie, product eliminators fst(e) and snd(e)), there are no basically issues whatsoever. The reason it took so long to figure out is because it turns out to be more natural to do eta expansions rather than eta reductions. See Barry Jay's The Virtues of Eta Expansion.

If you want products to have a pattern-style eliminator 

let (a,b) = e in t

Then matters are more complex. The primary difficulty with pattern matching are the commuting conversions. That is, these calculi have the equation 

C[let (a,b) = e in t] === let (a,b) = e in C[t]

and figuring out (a) which context C[-] to use and (b) how to orient this equation gets tricky. IMO, the state of the art for rewriting-style approaches are Sam Lindley's Extensional Rewriting with Sums and Gabriel Scherer's Deciding Equivalence with Sums and the Empty Type, both of which consider the typed lambda calculus with both products and sums.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.