Take the 2-minute tour ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

(I'm not sure if I should post this here rather than at Theoretical Computer Science, I've found a lot of type theory related questions on MathOverflow)

I'm working in Martin-Löf type theory with inductive types. Everything I say below for booleans should be understood with the type of booleans replaced by any inductive type, but for simplicity I'll do it in the case of boolean with match with written as if then else.

My question is about two reduction rules that I've never seen studied anywhere but that seems rather natural to me. I'd like to know if those rules have an "official" name and where I could read about them.

The first one (that I'm calling "lazy match") has the form

b : bool $\vdash$ if b then u else u $\rightarrow$ u : A

where A is a type, b : bool $\vdash$ u : A and "$\rightarrow$" is reduction (definitional equality, if you prefer).
I know there is a problem with this rule if b does not terminate, but I'm interested here in type theory as a logical system, so everything is supposed to terminate.

The second one (that I'm calling "deep match") is about exchanging two match and has the form

b : bool $\vdash$ if (if b then s else t) then u else v $\rightarrow$ if b then (if s then u else v) else (if t then u else v) : A

where A is a type, b : bool $\vdash$ s, t : bool and b : bool $\vdash$ u, v : A
Intuitively, when you match a match expression, the outer match can be distributed in the branches of the inner match.

Where can I read about these rules? Or are there obvious problems that I haven't seen? (there are perhaps problems with inductive predicates (as opposed to inductive types), but you can restrict it to inductive types)

share|improve this question
    
I would call the first rule $\eta$-rule. –  Andrej Bauer Jan 2 '12 at 18:42
1  
@Andrej I would rather call $\eta$-rule the rule if b then true else false $\rightarrow$ b, but with dependent pattern matching and the commuting conversions (my second rule and the other related rules written in "Proofs and Types"), this seems to be equivalent to my first rule. –  Guillaume Brunerie Jan 3 '12 at 12:17
add comment

2 Answers 2

up vote 7 down vote accepted

Your second reduction is called a commutative conversion. You can read about it in Girard, Taylor and Lafont, Proofs and Types, p. 80, for example. The congruence relation with commutative conversions for coproducts is has normal forms, see for instance:

Normalization by evaluation for typed lambda calculus with coproducts, by T. Altenkirch, P. Dybjer, M. Hofmann, and P. Scott

For a strongly normalizing reduction relation for commutative conversions, try:

Short Proofs of Normalization for the simply-typed lambda-calculus, permutative conversions and Gödel's T (1999) by Felix Joachimski , Ralph Matthes

(EDIT: Three more references. I haven't looked at these, but they sound helpful:)

Exceptional NbE for Sums by Freiric Barral

P. de Groote. Strong normalization of classical natural deduction with disjunction. In S. Abramsky, editor, Typed Lambda Calculi and Applications, volume 2044 of Lecture Notes in Computer Science, pages 182-196. Springer, 2001.

K. Nour and R. David. A short proof of the strong normalization of classical natural deduction with disjunction. The Journal of Symbolic Logic, 68(4):1277-1288, December 2003.

share|improve this answer
    
Thanks, this is very helpful, this is exactly the king of thing I was looking for. But something puzzles me, in the article they do not prove that this $\lambda$-calculus is strongly normalizing, they have a notion of normal form that are terms with a new construct $\mathcal{C}$. For example if you want to match two booleans (example 3.1.2), there are two different ways to do this, that are definitionally equal but cannot be reduced to each other, so this calculus is not even confluent. Perhaps that it can be fixed by allowing $\mathcal{C}$ in the syntax of terms. –  Guillaume Brunerie Jan 3 '12 at 12:56
    
Of course you're right that normalization by evaluation only produces normal forms for a congruence relation. For these eta-like rules you have to be careful I you want to extract a normalizing reduction relation, which is why normalization by evaluation seems preferable in this case. I've edited my answer to reflect this, and added another reference you might find helpful. –  Ulrik Buchholtz Jan 3 '12 at 18:38
    
Thanks again :-) –  Guillaume Brunerie Jan 4 '12 at 10:21
add comment

I think both rules are an instance of a more general relation:

b : bool ⊢ f (if b then x else y) ≡ if b then f x else f y : A

Your first rule is with f := const u, but going backwards. The second rule is with

f a := if a then u else v

I've used ≡ instead of an → since I'm not sure which is side more reduced.

I vaguely recall this being called either χ-conversion or ξ-conversion, but I forget. Perhaps someone else can help more.

share|improve this answer
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

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