New answers tagged lambda-calculus
5
It seems to me there isn't an agreement about what "HOL" means. The OP indicates in their question that they are thinking of the formalization of higher-order logic within the formalism of the simply-typed $\lambda$-calculus. To give the question some clarity, allow me to spell out my understanding of what such a formalism comprises.
Recall the ...
6
The structure you want is due to Andy Pitts, and is called a tripos. It extends the notion of hyperdoctrine, which gives a categorical model for first-order logic, with enough structure to model higher-order logic.
However, much more of the work in this part of categorical logic focuses on toposes instead of triposes, which are just a little bit more ...
8
The answer is no. An old theorem of Statman states that $\beta$-equivalence in the simply-typed $\lambda$-calculus is not elementary recursive, that is, no algorithm whose running time is bounded by $2^{\vdots^{2^{|S|+|T|}}}$ for a tower of exponentials of fixed height may decide whether two simply-typed terms $S$ and $T$ are $\beta$-equivalent.
The ...
Top 50 recent answers are included
