Anonymous

Programming Language Theory: Difference between revisions

From dankwiki
no edit summary
No edit summary
 
(6 intermediate revisions by the same user not shown)
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==
==Functions and Declarative Programming==
Line 19: Line 20:
The ''omega'' combinator is divergent. It can be reduced, but has no normal form:
The ''omega'' combinator is divergent. It can be reduced, but has no normal form:
* <tt>omega ≡ (λx. x x) (λx. x x)</tt>
* <tt>omega ≡ (λx. x x) (λx. x x)</tt>
A combinator which is in normal form, but not reduced to a value, is said to be ''stuck''. One of the major objective of static [[Programming_Language_Theory#Typing|typing systems]] is to detect possible "stuck" reductions.
A combinator which is in normal form, but not reduced to a value, is said to be ''stuck''. One of the major objectives of static [[Programming_Language_Theory#Typing|typing systems]] is to detect possible "stuck" reductions.


====Fixed-Point Combinators====
====Fixed-Point Combinators====
Line 44: Line 45:
λ-abst ::= '(' 'λ'var'.' λ-term ')'</pre>
λ-abst ::= '(' 'λ'var'.' λ-term ')'</pre>
====Evaluation via Substitution====
====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 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))
* If M is a λ-app ({N / X}(A B)), {N / X}M = (({N / X}A) ({N / X}B))
Line 189: Line 192:
==Concurrency==
==Concurrency==
*'''FIXME''' π-calculus, CSS, CSP, petri nets, dataflow variables...
*'''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 Design==
Line 210: Line 216:
* Van Roy and Haridi. [http://www.amazon.com/Concepts-Techniques-Models-Computer-Programming/dp/0262220695 ''Concepts, Techniques and Models of Computer Programming'']. MIT Press, 2004.
* Van Roy and Haridi. [http://www.amazon.com/Concepts-Techniques-Models-Computer-Programming/dp/0262220695 ''Concepts, Techniques and Models of Computer Programming'']. MIT Press, 2004.
* Pierce. [http://www.amazon.com/Types-Programming-Languages-Benjamin-Pierce/dp/0262162091 ''Types and Programming Languages'']. MIT Press, 2002.
* Pierce. [http://www.amazon.com/Types-Programming-Languages-Benjamin-Pierce/dp/0262162091 ''Types and Programming Languages'']. MIT Press, 2002.
* Culler and Singh. [http://www.eecs.berkeley.edu/~culler/book.alpha/ ''Parallel Computer Architecture: A Hardware/Software Approach'']. Morgan Kaufman, 1999.
* Felleisen. [http://www.ps.uni-sb.de/courses/sem-prog97/material/YYWorks.ps "A Lecture on the ''Why'' of ''Y''"]. 1997.
* Felleisen. [http://www.ps.uni-sb.de/courses/sem-prog97/material/YYWorks.ps "A Lecture on the ''Why'' of ''Y''"]. 1997.
* Winskel. [http://www.amazon.com/Formal-Semantics-Programming-Languages-Winskel/dp/0262731037 ''Formal Semantics of Programming Languages'']. MIT Press, 1993.
* Winskel. [http://www.amazon.com/Formal-Semantics-Programming-Languages-Winskel/dp/0262731037 ''Formal Semantics of Programming Languages'']. MIT Press, 1993.