0
$\begingroup$

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".

$\endgroup$

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.