Anonymous

Programming Language Theory: Difference between revisions

From dankwiki
no edit summary
No edit summary
 
(30 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 "topoi", "sheaves", "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 113: Line 116:
* Church suggested explicit type annotations on all terms (simply-typed λ-calculus (λ<sub>→</sub>), "simple" due to single type constructor →)
* Church suggested explicit type annotations on all terms (simply-typed λ-calculus (λ<sub>→</sub>), "simple" due to single type constructor →)
* Curry suggested inferred types (now implemented via techniques such as [http://en.wikipedia.org/wiki/Hindley-Milner_type_inference Hindley-Milner])
* Curry suggested inferred types (now implemented via techniques such as [http://en.wikipedia.org/wiki/Hindley-Milner_type_inference Hindley-Milner])
Either way, we lose some properties of the untyped λ-calculus (there's no type for the Y-combinator, for instance!). Nonetheless, the benefits of [[Programming_Language_Theory#Typing|typing]] (especially in the presence of type inference) lead to most functional programming languages making use of a strict typing system. More complicated systems (''second-'' and higher-''order  λ-calculi'') such as System F (aka Girard-Reynolds polymorphic λ-calculus) exist; they can be explored along Barendregt's [http://en.wikipedia.org/wiki/Lambda_cube λ-cube], should one feel so inclined.
Either way, we lose some properties of the untyped λ-calculus (there's no type for the Y-combinator, for instance!). Nonetheless, the benefits of [[Programming_Language_Theory#Typing|typing]] (especially in the presence of type inference) lead to most functional programming languages making use of a strict typing system. More complicated systems (''second-'' and higher-''order  λ-calculi'') such as System F (aka Girard-Reynolds polymorphic λ-calculus) and λ<sub>ω</sub> (aka "simply-typed λ-calculus with type operators") exist; they can be explored along Barendregt's [http://en.wikipedia.org/wiki/Lambda_cube λ-cube], should one feel so inclined (unravel the mysteries of "F<sub>&lt;:</sub><sup>ω</sup>"!).


===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 125: Line 162:


==Typing==
==Typing==
Weak- vs strong-typing refers to the degree to which the language's typing system can be subverted, and whether this is regularly necessary. Static- vs dynamic-typing refers to (among other possible definitions) whether type is determined at compile-time or run-time. Among dynamic typing, ''duck typing'' types based on (dynamically-bound) method availability; variants of static typing include ''structural typing'' (relations based on form) and ''nominative typing'' (relations based on names). The benefits of static typing include:
Weak- vs strong-typing refers to the degree to which the language's typing system can be subverted, and whether this is regularly necessary. Typing insecurities include:
* Untyped pointers
* Subrange narrowing / downcasting
* Untagged variant records ("type punning")
* Procedure parameters
Static- vs dynamic-typing refers to (among other possible definitions) whether type is determined at compile-time or run-time. Among dynamic typing, ''duck typing'' types based on (dynamically-bound) method availability; variants of static typing include ''structural typing'' (relations based on form) and ''nominative typing'' (relations based on names). Nominative typing has (predictable) problems with anonymous types, and also name shadowing. Structural typing has issues with recursive declarations, along with ambiguities regarding constituent ordering and nomenclature; it is used primarily in ML and research, with nominative typing dominating the mainstream. The benefits of static typing include:
* Detection of many types of errors at compile-time
* Detection of many types of errors at compile-time
** "Safety = Progress + Preservation" (Harper 1994) suggests well-typed expressions ought not get [[Programming_Language_Theory#Divergent_Combinators|stuck]], and that reductions of well-typed expressions are themselves well-typed.
** "Safety = Progress + Preservation" (Harper 1994) suggests well-typed expressions ought not get [[Programming_Language_Theory#Divergent_Combinators|stuck]], and that reductions of well-typed expressions are themselves well-typed.
Line 133: Line 175:
* Support for ''polymorphism'' (dispatch based on types of actual arguments)
* Support for ''polymorphism'' (dispatch based on types of actual arguments)
** Parametric polymorphism: Generation of a version for necessary types (Ada generics, C++ templates, SML type parameters)
** Parametric polymorphism: Generation of a version for necessary types (Ada generics, C++ templates, SML type parameters)
* Support for ''subtyping''
* Support for ''subtyping'', refining T as T<sub>0</sub> (defining an ordering relation on types: T ''subsumes'' T<sub>0</sub>, x ∈ T<sub>0</sub> ⇒ x ∈ T)
** '''NB''': ''Subclassing'' (inheritance) is independent of subtyping!
** Subsumption properties can't be arbitrarily enforced (decided) when subclasses override the implementation
** ''Soundness'' refers to data structuring operation support for subtyping, such as annotation of type alterations:
*** ''Covariant'' modifications retain the original ordering
*** ''Contravariant'' modifications invert the original ordering
*** ''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===
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''.


==Objects==
==Objects==
Line 141: 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 162: 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.