Anonymous

Programming Language Theory: Difference between revisions

From dankwiki
no edit summary
No edit summary
 
(15 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 116: Line 119:


===Logic Programming===
===Logic Programming===
'''FIXME''' unification, backtracking, cuts
Non-procedural statements of relationships built atop a ''unification'' algorithm and database.
====Prolog====
Language elements include facts, queries, variables, rules and data structures. Queries are made relative to a base of facts expressed as ''functors'' on ''atoms''. Anonymous variables are supported via '_'.
* All satisfactions of a query are returned, as they're discovered.
* Several queries can be conjoined via ','; unification of such a system might require ''backtracking''.
* Rules are dependencies among facts, expressed as unions of intersections (multiple right-hand-sides, each with arbitrarily many conjunctions). For <tt>a :- b, c</tt>:
** Backward chaining -- seeking truth of <tt>a</tt> via proof of <tt>b, c</tt>
** Forward chaining -- concluding truth of <tt>a</tt> via discovery of <tt>b, c</tt>
* Lists are formed via square brackets, and '|' divides the car and cdr of a list
Two semantics: declarative (first-order predicate logic) and procedural (DFS of the database).
* The procedural semantics involve terms (constants, atoms, functors), ground terms (a term containing no variables), and the resolvent (set of all outstanding subgoals).
** Queries with no variables can trivially be decided as true or false
** The result is otherwise the set of all query-satisfying bindings between variables and ground terms
** Resolvent grows when a RHS is substituted for a subgoal
** Resolvent shrinks when a fact matches a subgoal
** ''Logically-incomplete'': DFS might fail on left-recursive rules. BFS takes up a great deal of space.
* The declarative semantics reduce the resolvent processing to modus ponens:
** Any Prolog program can be represented as a set of Horn clauses...which can be transformed into clausal predicate logic...which can be transformed into predicate logic
** A Horn clause is a set of terms, exactly one of which is positive
*** A clause with no negative terms corresponds to a Prolog fact
*** The single positive term corresponds to the LHS of a Prolog rule
*** The zero or more negative terms correspond to clauses on the RHS:
* The ''cut'' operator '!' controls searching: "No further options for the current rule ought be considered"
** The declarative semantics are unaffected
** Whether or not procedural semantics generate solutions might change, but not the solutions generated
 
{| border="1"
! Prolog statement
! Logical interpretation
! Horn clause (Implicitly-quantified CNF)
|-
| A :- B || B ⇒ A || ~B ∨ A
|-
| A :- B, C, D || B ∧ C ∧ D ⇒ A ≡ ~(B ∧ C ∧ D) ∨ A || ~B ∨ ~C ∨ ~D ∨ A
|}


===Constraint Programming===
===Constraint Programming===
Line 146: Line 183:
*** ''Invariant'' modifications dissolve the subsumption relation
*** ''Invariant'' modifications dissolve the subsumption relation
* Support for ''minimal'' and ''maximal'' types (also known as Bottom and Top)
* Support for ''minimal'' and ''maximal'' types (also known as Bottom and Top)
** Bottom (no values) + Top (all values) + subtyping ⇒ ''bounded type lattice''
===Conversion===
===Conversion===
Treatment of a value of a given type as if it had another type, possibly involving modification of the underlying representation, or storage/alignment requirements thereof. When done explicitly, conversion is referred to as ''casting''; when done implicitly, it is called ''coercion''.
Treatment of a value of a given type as if it had another type, possibly involving modification of the underlying representation, or storage/alignment requirements thereof. When done explicitly, conversion is referred to as ''casting''; when done implicitly, it is called ''coercion''.
Line 154: 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 175: 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.