A second order theory of infinite trees

Abstract

An axiomatic approach based on second order logic for specifying finite data types has been given in [12]. In the present paper we generalize the approach to infinite trees. Data logic CT of infinite trees is introduced and investigated. CT is based on the data logic T of finite trees. For treating infinite objects we heavily rely upon the notions of Bishop'apos;s constructive mathematics. Thus the results of the present paper are closely related with an intuitionistic type theory of infinite trees.

Keywords:

• Infinite trees
• second order theory
• data logic
• constructive mathematics

C.R.Categories:

• D.3.3
• E.1
• F.3.3