Questions

Researchers are aiming at theorems. I always like the origin of the word ‘theorem’, its etymology, that I once dug up. It has the same linguistic source as theater and theos. Its meaning is ‘that what one sees’. I hope experts can confirm this linguistic tracing.

But there is something preceding theorems. Namely Questions.In this part of the website I collect many questions that arose in my work during half a century, collected in a couple of dozens of Notebooks, sometimes at the end of research papers, in e.g. Concluding Remarks and Questions, or ‘Future Directions’.

Or in Research Proposals submitted to acquire national or European funding for our group’s research, and that were not succesful. In our group’s best times we had a favourable score of 1 out of 3 proposals being succesful; the general average of success was one in six. So several proposals, often requiring month’s work, were shelved and forgotten. It would be nice if you could publish them om say, arxive, the highly useful current repository for recent research papers.

How long lasts transfinite rewriting?

Is there for every recursive countable ordinal alpha a finite lambda term, normalizing, with transfinite reduction to its normal form of length alpha? See this note from 2008 with a tentative solution for orthogonal term rewrite systems, devised by Ariya Isihara during his PhD-period at the Vrije Universiteit Amsterdam from 2006-2010. It is likely that we can translate his TRS on page 10 to the lambda calculus. Ariya’s TRS implements the Veblen hierarchy of ordinals, including the giant ordinals like Gamma-0.

Another question on this Veblen hierarchy of countable ordinals is suggested by the Veblen matrix figure: the countable ordinals appearing as entries in this matrix have in general multiple notations. So what is the equality theory that is at stake here? Can it be captured in a nice TRS?

This is just a question from a non-expert in ordinal notations and the amazing varieties in large ordinals. Originating from curiosity about how long transfinite rewrite sequences can be. For infinite lambds terms it is easy to see that every countable ordinal can be a reduction length. For finite lambda terms we get likely all ordinals less than Omega-Church-Kleene.