Programming Language Theory: Difference between revisions

(4 intermediate revisions by the same user not shown)

Line 1:

The Church-Turing Thesis equates a vaguely-defined set of "computable" functions with the [http://en.wikipedia.org/wiki/Computable_function partial recursive functions]. Several systems have been proven equivalent to the partial recursives in power, such as Turing machines and the λ-calculus (practical programming languages generally provide further syntaxes and semantics, but a [[Real Programmer]] is perfectly happy with combinatory logic and a beer). Peter J. Landin's 1965 ACM report, "A correspondence between ALGOL 60 and Church's Lambda-notation", is blamed by most textbooks for jump-starting the study of programming language theory, ensuring computer scientists ~~forty~~ years later would still be exploring "[http://en.wikipedia.org/wiki/Topos topoi]", "[http://en.wikipedia.org/wiki/Sheaf_theory sheaves]", "[http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence Curry-Howard correspondences]" and "fixed-point combinators".<blockquote>''There may, indeed, be other applications of the system than its use as a logic.'' -- Alonzo Church, 1932</blockquote>

[[CATEGORY: CS GRE Prep]]

The Church-Turing Thesis equates a vaguely-defined set of "computable" functions with the [http://en.wikipedia.org/wiki/Computable_function partial recursive functions]. Several systems have been proven equivalent to the partial recursives in power, such as Turing machines and the λ-calculus (practical programming languages generally provide further syntaxes and semantics, but a [[Real Programmer]] is perfectly happy with combinatory logic and a beer). Peter J. Landin's 1965 ACM report, "A correspondence between ALGOL 60 and Church's Lambda-notation", is blamed by most textbooks for jump-starting the study of programming language theory, ensuring computer scientists fifty years later would still be exploring [http://en.wikipedia.org/wiki/Topos topoi], [http://en.wikipedia.org/wiki/Sheaf_theory sheaves], [http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence Curry-Howard correspondences] and fixed-point combinators.<blockquote>''There may, indeed, be other applications of the system than its use as a logic.'' -- Alonzo Church, 1932</blockquote>

==Functions and Declarative Programming==

Line 44:

Line 45:

λ-abst ::= '(' 'λ'var'.' λ-term ')'</pre>

====Evaluation via Substitution====

We'll use a substitution syntax to rewrite λ-calculus strings. Heavyweight [http://en.wikipedia.org/wiki/De_Bruijn_notation de Bruijn indexing] is one substitution semantic, as is the ''Barendregt convention''. The following simple semantic is due Rugaber, possibly through Pierce: ''{N / X}M'' substitutes expression N for free instances of X in expression M:

We'll use a substitution syntax to rewrite λ-calculus strings. Heavyweight [http://en.wikipedia.org/wiki/De_Bruijn_notation de Bruijn indexing] is one substitution semantic, as is the ''Barendregt convention''. The following simple semantic is due Rugaber, possibly through Pierce:

''{N / X}M'' substitutes expression N for free instances of X in expression M:

* If M is a variable ({N / X}V), replace M with X if and only if M is N.

* If M is a λ-app ({N / X}(A B)), {N / X}M = (({N / X}A) ({N / X}B))

Line 189:

Line 192:

==Concurrency==

*'''FIXME''' π-calculus, CSS, CSP, petri nets, dataflow variables...

*~~'''~~FIXME~~''' message-passing, shared-state~~

* Shared state

* Message passing

* Data parallel processing

* FIXME expand each

==Programming Language Design==

@@ Line 1: / Line 1: @@
-The Church-Turing Thesis equates a vaguely-defined set of "computable" functions with the [http://en.wikipedia.org/wiki/Computable_function partial recursive functions]. Several systems have been proven equivalent to the partial recursives in power, such as Turing machines and the λ-calculus (practical programming languages generally provide further syntaxes and semantics, but a [[Real Programmer]] is perfectly happy with combinatory logic and a beer). Peter J. Landin's 1965 ACM report, "A correspondence between ALGOL 60 and Church's Lambda-notation", is blamed by most textbooks for jump-starting the study of programming language theory, ensuring computer scientists forty years later would still be exploring "[http://en.wikipedia.org/wiki/Topos topoi]", "[http://en.wikipedia.org/wiki/Sheaf_theory sheaves]", "[http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence Curry-Howard correspondences]" and "fixed-point combinators".<blockquote>''There may, indeed, be other applications of the system than its use as a logic.'' -- Alonzo Church, 1932</blockquote>
+[[CATEGORY: CS GRE Prep]]
+The Church-Turing Thesis equates a vaguely-defined set of "computable" functions with the [http://en.wikipedia.org/wiki/Computable_function partial recursive functions]. Several systems have been proven equivalent to the partial recursives in power, such as Turing machines and the λ-calculus (practical programming languages generally provide further syntaxes and semantics, but a [[Real Programmer]] is perfectly happy with combinatory logic and a beer). Peter J. Landin's 1965 ACM report, "A correspondence between ALGOL 60 and Church's Lambda-notation", is blamed by most textbooks for jump-starting the study of programming language theory, ensuring computer scientists fifty years later would still be exploring [http://en.wikipedia.org/wiki/Topos topoi], [http://en.wikipedia.org/wiki/Sheaf_theory sheaves], [http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence Curry-Howard correspondences] and fixed-point combinators.<blockquote>''There may, indeed, be other applications of the system than its use as a logic.'' -- Alonzo Church, 1932</blockquote>
 ==Functions and Declarative Programming==
@@ Line 44: / Line 45: @@
 λ-abst ::= '(' 'λ'var'.' λ-term ')'</pre>
 ====Evaluation via Substitution====
-We'll use a substitution syntax to rewrite λ-calculus strings. Heavyweight [http://en.wikipedia.org/wiki/De_Bruijn_notation de Bruijn indexing] is one substitution semantic, as is the ''Barendregt convention''. The following simple semantic is due Rugaber, possibly through Pierce: ''{N / X}M'' substitutes expression N for free instances of X in expression M:
+We'll use a substitution syntax to rewrite λ-calculus strings. Heavyweight [http://en.wikipedia.org/wiki/De_Bruijn_notation de Bruijn indexing] is one substitution semantic, as is the ''Barendregt convention''. The following simple semantic is due Rugaber, possibly through Pierce:
+''{N / X}M'' substitutes expression N for free instances of X in expression M:
 * If M is a variable ({N / X}V), replace M with X if and only if M is N.
 * If M is a λ-app ({N / X}(A B)), {N / X}M = (({N / X}A) ({N / X}B))
@@ Line 189: / Line 192: @@
 ==Concurrency==
 *'''FIXME''' π-calculus, CSS, CSP, petri nets, dataflow variables...
-*'''FIXME''' message-passing, shared-state
+* Shared state
+* Message passing
+* Data parallel processing
+* FIXME expand each
 ==Programming Language Design==

Programming Language Theory: Difference between revisions

Dank (talk | contribs)