Expressive power of typed and type-free programming languages (Q761790): Difference between revisions

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.

0 references

Mathematics Subject Classification ID

68Q60

0 references

0 references

0 references

0 references

0 references

0 references

type theory

0 references

lambda-calculus

0 references

type-free programming concepts

0 references

typed lambda-schemes

0 references

formal semantics

0 references

describes a project that uses

0 references

0 references

0 references

MaRDI publication profile

0 references

full work available at URL

https://doi.org/10.1016/0304-3975(84)90088-4

0 references

OpenAlex ID

W2081900912

0 references

cites work

A draft description of Pascal

0 references

Least fixed points revisited

0 references

Q5649409

0 references

A global representation of the recursive functions in the $\lambda$- calculus

0 references

The lambda calculus, its syntax and semantics

0 references

0 references

0 references

0 references

0 references

0 references

0 references

On Classes of Program Schemata

0 references

Q5565113

0 references

Combinatory logic. Vol. II

0 references

Q4172933

0 references

Q4151140

0 references

Q4156412

0 references

Simple program schemes and formal languages

0 references

IO and OI. II

0 references

Q4070302

0 references

Q3904045

0 references

Initial Algebra Semantics and Continuous Algebras

0 references

Theory of program structures: Schemes, semantics, verification

0 references

0 references

0 references

0 references

0 references

0 references

0 references

0 references

0 references

Correspondence between ALGOL 60 and Church's Lambda-notation

0 references

On procedures as open subroutines. II

0 references

0 references

0 references

0 references

0 references

Algebraic automata and context-free sets

0 references

Q4133080

0 references

Q4138713

0 references

Fully abstract models of typed $\lambda$-calculi

0 references

λ-definierbare Funktionen auf Peanoalgebren

0 references

The Standardization Theorem for λ‐Calculus

0 references

Q4124819

0 references

Q4116078

0 references

Q4185781

0 references

LCF considered as a programming language

0 references

Q5573961

0 references

Q5649639

0 references

Data Types as Lattices

0 references

Q5685626

0 references

The Relation between Computational and Denotational Properties for Scott’s ${\text{D}}_\infty $-Models of the Lambda-Calculus

0 references

Approximate Reduction and Lambda Calculus Models

0 references

Q4182475

0 references

The programming language Pascal

0 references

Sitelinks

Mathematics(1 entry)

mardi Publication:761790

@@ Property / cites work @@
+A draft description of Pascal
@@ Property / cites work: A draft description of Pascal / rank @@
+Normal rank
@@ Property / cites work @@
+Least fixed points revisited
@@ Property / cites work: Least fixed points revisited / rank @@
+Normal rank
@@ Property / cites work @@
+Q5649409
@@ Property / cites work: Q5649409 / rank @@
+Normal rank
@@ Property / cites work @@
+A global representation of the recursive functions in the \(\lambda\)- calculus
+Normal rank
@@ Property / cites work @@
+The lambda calculus, its syntax and semantics
@@ Property / cites work: The lambda calculus, its syntax and semantics / rank @@
+Normal rank
@@ Property / cites work @@
+Q4160405
@@ Property / cites work: Q4160405 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3205213
@@ Property / cites work: Q3205213 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5531462
@@ Property / cites work: Q5531462 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4068081
@@ Property / cites work: Q4068081 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4109650
@@ Property / cites work: Q4109650 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5618896
@@ Property / cites work: Q5618896 / rank @@
+Normal rank
@@ Property / cites work @@
+On Classes of Program Schemata
@@ Property / cites work: On Classes of Program Schemata / rank @@
+Normal rank
@@ Property / cites work @@
+Q5565113
@@ Property / cites work: Q5565113 / rank @@
+Normal rank
@@ Property / cites work @@
+Combinatory logic. Vol. II
@@ Property / cites work: Combinatory logic. Vol. II / rank @@
+Normal rank
@@ Property / cites work @@
+Q4172933
@@ Property / cites work: Q4172933 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4151140
@@ Property / cites work: Q4151140 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4156412
@@ Property / cites work: Q4156412 / rank @@
+Normal rank
@@ Property / cites work @@
+Simple program schemes and formal languages
@@ Property / cites work: Simple program schemes and formal languages / rank @@
+Normal rank
@@ Property / cites work @@
+IO and OI. II
@@ Property / cites work: IO and OI. II / rank @@
+Normal rank
@@ Property / cites work @@
+Q4070302
@@ Property / cites work: Q4070302 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3904045
@@ Property / cites work: Q3904045 / rank @@
+Normal rank
@@ Property / cites work @@
+Initial Algebra Semantics and Continuous Algebras
@@ Property / cites work: Initial Algebra Semantics and Continuous Algebras / rank @@
+Normal rank
@@ Property / cites work @@
+Theory of program structures: Schemes, semantics, verification
+Normal rank
@@ Property / cites work @@
+Q4163516
@@ Property / cites work: Q4163516 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5686017
@@ Property / cites work: Q5686017 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3681911
@@ Property / cites work: Q3681911 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5592246
@@ Property / cites work: Q5592246 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4101793
@@ Property / cites work: Q4101793 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4070337
@@ Property / cites work: Q4070337 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4105238
@@ Property / cites work: Q4105238 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4766569
@@ Property / cites work: Q4766569 / rank @@
+Normal rank
@@ Property / cites work @@
+Correspondence between ALGOL 60 and Church's Lambda-notation
+Normal rank
@@ Property / cites work @@
+On procedures as open subroutines. II
@@ Property / cites work: On procedures as open subroutines. II / rank @@
+Normal rank
@@ Property / cites work @@
+Q5636311
@@ Property / cites work: Q5636311 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4101795
@@ Property / cites work: Q4101795 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4174202
@@ Property / cites work: Q4174202 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4766020
@@ Property / cites work: Q4766020 / rank @@
+Normal rank
@@ Property / cites work @@
+Algebraic automata and context-free sets
@@ Property / cites work: Algebraic automata and context-free sets / rank @@
+Normal rank
@@ Property / cites work @@
+Q4133080
@@ Property / cites work: Q4133080 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4138713
@@ Property / cites work: Q4138713 / rank @@
+Normal rank
@@ Property / cites work @@
+Fully abstract models of typed \(\lambda\)-calculi
+Normal rank
@@ Property / cites work @@
+λ-definierbare Funktionen auf Peanoalgebren
@@ Property / cites work: λ-definierbare Funktionen auf Peanoalgebren / rank @@
+Normal rank
@@ Property / cites work @@
+The Standardization Theorem for λ‐Calculus
@@ Property / cites work: The Standardization Theorem for λ‐Calculus / rank @@
+Normal rank
@@ Property / cites work @@
+Q4124819
@@ Property / cites work: Q4124819 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4116078
@@ Property / cites work: Q4116078 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4185781
@@ Property / cites work: Q4185781 / rank @@
+Normal rank
@@ Property / cites work @@
+LCF considered as a programming language
@@ Property / cites work: LCF considered as a programming language / rank @@
+Normal rank
@@ Property / cites work @@
+Q5573961
@@ Property / cites work: Q5573961 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5649639
@@ Property / cites work: Q5649639 / rank @@
+Normal rank
@@ Property / cites work @@
+Data Types as Lattices
@@ Property / cites work: Data Types as Lattices / rank @@
+Normal rank
@@ Property / cites work @@
+Q5685626
@@ Property / cites work: Q5685626 / rank @@
+Normal rank
@@ Property / cites work @@
+The Relation between Computational and Denotational Properties for Scott’s ${\text{D}}_\infty  $-Models of the Lambda-Calculus
+Normal rank
@@ Property / cites work @@
+Approximate Reduction and Lambda Calculus Models
@@ Property / cites work: Approximate Reduction and Lambda Calculus Models / rank @@
+Normal rank
@@ Property / cites work @@
+Q4182475
@@ Property / cites work: Q4182475 / rank @@
+Normal rank
@@ Property / cites work @@
+The programming language Pascal
@@ Property / cites work: The programming language Pascal / rank @@
+Normal rank