Is my lambda calculus reduction correct and final form valid in simply typed lambda calc? I'm looking at some lambda calculus at the moment and came across this question:

0:R

1:R

plus: R->R->R

(lambda f:T . lambda g:U . (f 0) (g 0)) (plus 1) (plus (plus 1 1))

Is it well typed given appropriate types for T and U?

I'm new to lambda calc but I gather that we substitute (plus 1) for f and (plus (plus 1 1)) for g.

This will reduce to
(plus 1 0) (plus (plus 1 1) 0)
The right hand side (plus 1 1) will reduce to an R and then we will have (plus R 0) which will reduce to an R. The left side will reduce to an R so the whole expression reduces to the form R R.

Is this correct? Then f and g are of type R -> R (from currying) to make it valid. Is it an issue that the final expression will be of the form R R. Does this mean R gets applied to R then, so R would have to be an 'automorphic' function (mapping from a type to the same type)... is this something related to not having recursion in simply typed lambda calc?
While your way of calculating the types isn't quite how it works, it gives the right answer here. As you say, you end up with f 0 having type R and g 0 having type R. Since we apply f 0 to g 0, R must be of the form R -&gt; X for some X. In other words, you have the equi-recursive type R = R -&gt; X. Such types are almost always disallowed. Thus, this would be a type error. If R is a fixed primitive type, e.g. a type of primitive natural numbers, then it is simply not the case that R = R -&gt; X and so you would also get a type error.