Weakly normalizing + confluent = strongly normalizing? I was reading this abstract and saw that they prove weak normalization and confluence. My limited understanding suggests that those two properties should provide strong normalization, which then leaves me confused about why they'd leave that out in the abstract, thus suggesting I might be wrong.

Is it the case that a confluent weakly normalizing system is strongly normalizing? Why/why not?
Is it the case that a confluent weakly normalizing system is strongly normalizing?  Why/why not?


No, it's not necessarily the case. 


Weak normalization means: there exists a reduction strategy that will lead to a normal form. 
People often use confluence to mean what rewriting people call "local confluence": this is the property that if $a \leadsto b$ and $a \leadsto c$, then $b$ and $c$ can be joined -- i.e., there exists a $d$ such that $b \leadsto^\ast d$ and $c \leadsto^\ast d$. 


This does not rule out the existence of infinite reduction sequences. 

As an example, start with the STLC and add a new base type $X$ and constant $c,d : X$ with the reduction rule $c \leadsto c$ and $c \leadsto d$.

There is a weak normalization strategy: use a weak normalization strategy for the STLC and immediately reduce any $c$ to $d$. The calculus is also Church-Rosser, since it inherits this property from the STLC. But it isn't strongly normalizing since you can reduce a $c$ forever.