I am attempting to implement Simple Type Theory in the language D. How do you compare subterms to a term $R$ for the sake of computing the covering abstractors of $R$ in $M$?

By reference (class objects), syntactically by string value, or by some defined equality function?

Definition. (Body, scope, covering abstractors) Let $\lambda x.P$ be a component of a term $M$. The displayed component $P$ is called the body of or the scope of the abstractor $\lambda x$.

The covering abstractors of a component $R$ of $M$ are the abstractors in $M$ whose scopes contain $R$.

This is from the book "Basic Simple Type Theory".


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.