Semantics of Propositional Attitudes in Type-Theory of Algorithms

In this paper, I introduce the extended type-theory of acyclic algorithms \({\text {L}}^{\lambda }_{\textrm{ar}}\) and its version \({\text {L}}^{\lambda }_{r}\) with full recursion. The extended theory and its reduction calculus provide algorithmic semantics of attitude expressions, including beliefs, knowledge, and statements, which are present in advanced applications requiring computational semantics of natural language. The extended type-theory of algorithms includes restrictor terms, terms of logic operators, and pure quantifiers. The restrictor terms have effects of presuppositional restrictions, requiring objects to have certain properties. I provide brief, while important information on the relation of the theory of recursion \({\text {L}}^{\lambda }_{r}\) to the formal language LCF of \(\lambda \) -calculus, by Dana S. Scott and Gordon Plotkin, covering let-expressions for semantics of programming langages.