Programming Language Theory - revision history

Dank at 21:09, 5 August 2011

2011-08-05T21:09:09Z

← Older revision		Revision as of 21:09, 5 August 2011
Line 1:		Line 1:
	[[CATEGORY: CS GRE Prep]]		[[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 ~~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>		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==

Dank at 04:16, 28 June 2011

2011-06-28T04:16:50Z

← Older revision		Revision as of 04:16, 28 June 2011
Line 1:		Line 1:
	[[CATEGORY: CS GRE]]		[[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 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>		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>

Dank at 04:16, 28 June 2011

2011-06-28T04:16:30Z

← Older revision		Revision as of 04:16, 28 June 2011
Line 1:		Line 1:
			[[CATEGORY: CS GRE]]
	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>		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>

Dank: /* Evaluation via Substitution */

2010-05-03T03:55:57Z

Evaluation via Substitution

← Older revision		Revision as of 03:55, 3 May 2010
Line 44:		Line 44:
	λ-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))

Dank: /* Concurrency */

2010-04-26T22:50:10Z

Concurrency

← Older revision		Revision as of 22:50, 26 April 2010
Line 189:		Line 189:
	==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==

Dank: /* Sources */

2010-04-26T22:17:51Z

Sources

← Older revision		Revision as of 22:17, 26 April 2010
Line 210:		Line 210:
	* 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.

Dank: /* Divergent Combinators */

2010-03-12T22:16:34Z

Divergent Combinators

← Older revision		Revision as of 22:16, 12 March 2010
Line 19:		Line 19:
	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====

Dank: /* Prolog */

2009-12-07T21:50:21Z

Prolog

← Older revision		Revision as of 21:50, 7 December 2009
Line 138:		Line 138:
	*** The single positive term corresponds to the LHS of a Prolog rule		*** 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 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"		{\| border="1"
	! Prolog statement		! Prolog statement

Dank: /* Prolog */

2009-12-07T20:38:55Z

Prolog

← Older revision		Revision as of 20:38, 7 December 2009
Line 141:		Line 141:
	! Prolog statement		! Prolog statement
	! Logical interpretation		! Logical interpretation
	! Horn clause		! Horn clause (Implicitly-quantified CNF)
	\|-		\|-
	\| A :- B \|\| B ⇒ A \|\| ~B ∨ A		\| A :- B \|\| B ⇒ A \|\| ~B ∨ A

Dank: /* Prolog */

2009-12-07T20:37:53Z

Prolog

← Older revision		Revision as of 20:37, 7 December 2009
Line 145:		Line 145:
	\| A :- B \|\| B ⇒ A \|\| ~B ∨ A		\| A :- B \|\| B ⇒ A \|\| ~B ∨ A
	\|-		\|-
	\| A :- B, C, D \|\| B ∧ C ∧ D ⇒ A \|\| ~B ∨ ~C ∨ ~D ∨ A		\| A :- B, C, D \|\| B ∧ C ∧ D ⇒ A ≡ ~(B ∧ C ∧ D) ∨ A \|\| ~B ∨ ~C ∨ ~D ∨ A
	\|}		\|}