Programming Language Theory: Difference between revisions

(14 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 19:

Line 20:

The ''omega'' combinator is divergent. It can be reduced, but has no normal form:

* <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====

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 116:

Line 119:

===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===

Line 155:

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 176:

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.

* 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.

* Winskel. [http://www.amazon.com/Formal-Semantics-Programming-Languages-Winskel/dp/0262731037 ''Formal Semantics of Programming Languages'']. MIT Press, 1993.

@@ 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 19: / Line 20: @@
 The ''omega'' combinator is divergent. It can be reduced, but has no normal form:
 * <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====
@@ 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 116: / Line 119: @@
 ===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===
@@ Line 155: / 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 176: / 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.
 * 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.
 * Winskel. [http://www.amazon.com/Formal-Semantics-Programming-Languages-Winskel/dp/0262731037 ''Formal Semantics of Programming Languages'']. MIT Press, 1993.

Programming Language Theory: Difference between revisions

Dank (talk | contribs)