Expressive power of typed and type-free programming languages

Combinatory logic and lambda calculus (03B40) Computability and recursion theory on ordinals, admissible sets, etc. (03D60) General topics in the theory of software (68N01) Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65)

Review text

The paper investigates the influence of type-free programming concepts on the definability of functions and objects in comparison with the exclusive use of typed concepts plus fixed-point operators. The underlying schemes are the classes of type-free and typed lambda-schemes respectively. The formal semantics of both classes are analyzed in the same semantical domains. In particular it is shown that typed lambda- schemes are translatable into equivalent type-free lambda-schemes but not vice verse. Furthermore, it is proved that the class of type-free lambda- schemes is universal in the sense that in the initial models all recursively enumerable \(\Sigma\)-trees (where \(\Sigma\) is the set of operation symbols) are definable.

Recommendations

Cites work

Cited in

(4)

Describes a project that uses

Uses Software

This page was built for publication: Expressive power of typed and type-free programming languages

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q761790)