> If the Epigram is not Turing complete, then what kind of programs cannot be expressed in it?
I think one quick answer for questions like this is "an interpreter for $LANGUAGE". The reason is that, for a language in which all programs terminate, a type-checked program is a proof that the algorithm terminates. Thus, an interpreter for $SOMEPL in $LANGUAGE is a proof that there is an interpreter for $SOMEPL that terminates on all input.
If $SOMEPL is $LANGUAGE, you get a Goedel/Halting-problem problem.
This is all, of course, assuming that "interpreter" means "function taking as input a valid program and outputting some finite data containing its normalized form". If you define an interpreter to just be a function that performs one step of evaluation, you can get away with it.
I think one quick answer for questions like this is "an interpreter for $LANGUAGE". The reason is that, for a language in which all programs terminate, a type-checked program is a proof that the algorithm terminates. Thus, an interpreter for $SOMEPL in $LANGUAGE is a proof that there is an interpreter for $SOMEPL that terminates on all input.
If $SOMEPL is $LANGUAGE, you get a Goedel/Halting-problem problem.
This is all, of course, assuming that "interpreter" means "function taking as input a valid program and outputting some finite data containing its normalized form". If you define an interpreter to just be a function that performs one step of evaluation, you can get away with it.