Subject reduction is a well and widely used property of typed rewriting systems.
Subject expansion is much less known.
What are the applications of this property and which systems enjoy it?

  • $\begingroup$ Would you care to explain or give a reference to "subject expansion"? What is it supposed to be? I suppose you mean the one mentioned by Wikipedia? The question is still too wide and unclear. $\endgroup$ – Andrej Bauer Aug 14 '18 at 22:38
  • $\begingroup$ Hey Andrej, I tried to make the question specific, but perhaps I could just ask "what is subject expansion?". I've seen it defined or used here, here and here. I have an intuition that it is somehow strongly related to the property of intersection type systems of characterizing normalizable terms. But that's a specutlation and I did not want to include it in the question. $\endgroup$ – Łukasz Lew Aug 15 '18 at 17:07

Your Answer

By clicking "Post Your Answer", you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.