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 acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Browse other questions tagged or ask your own question.