The Twelf Project - Recent changes [en]

User:Zoren

2010-09-06T12:11:52Z

New user account

Metatheorem

2010-09-06T10:31:48Z

← Older revision		Revision as of 10:31, 6 September 2010
Line 64:		Line 64:

	The proof term <math>\texttt{p-s}(\texttt{p-s}(\texttt{p-z}))</math> can be thought of as having the type <math>\texttt{plus}(\texttt{s}(\texttt{s}(0)),\;\texttt{s}(0),\;\texttt{s}(\texttt{s}(\texttt{s}(0))))</math>, but it can also be thought of as having the type		The proof term <math>\texttt{p-s}(\texttt{p-s}(\texttt{p-z}))</math> can be thought of as having the type <math>\texttt{plus}(\texttt{s}(\texttt{s}(0)),\;\texttt{s}(0),\;\texttt{s}(\texttt{s}(\texttt{s}(0))))</math>, but it can also be thought of as having the type
-	<math>\texttt{plus}(\texttt{s}(\texttt{s}(0)),\;0)\;\texttt{s}(\texttt{s}(0)))</math>. Remembering our analysis above, we can see that the most general type we can give the proof object <math>\texttt{p-s}(\texttt{p-s}(\texttt{p-z}))</math> is <math>(\forall N:\textit{nat}.\;\texttt{plus}(\texttt{s}(\texttt{s}(0)),\;N,\;\texttt{s}(\texttt{s}(N))))</math>.	+	<math>\texttt{plus}(\texttt{s}(\texttt{s}(0)),\;0,\;\texttt{s}(\texttt{s}(0)))</math>. Remembering our analysis above, we can see that the most general type we can give the proof object <math>\texttt{p-s}(\texttt{p-s}(\texttt{p-z}))</math> is <math>(\forall N:\textit{nat}.\;\texttt{plus}(\texttt{s}(\texttt{s}(0)),\;N,\;\texttt{s}(\texttt{s}(N))))</math>.

	=== Proving {{forall}}{{exists}}-statements using totality assertions ===		=== Proving {{forall}}{{exists}}-statements using totality assertions ===

Uniqueness lemma

2010-09-02T12:33:27Z

← Older revision		Revision as of 12:33, 2 September 2010
Line 37:		Line 37:

	Thus, we can prove the theorem by exhibiting the following total relation:		Thus, we can prove the theorem by exhibiting the following total relation:
-	<twelf check="true" ~~name~~="alt">	+	<twelf check="true" export="alt">
	bit-flip-unique : bit-flip B1 B2		bit-flip-unique : bit-flip B1 B2
	-> bit-flip B1 B2'		-> bit-flip B1 B2'
Line 57:		Line 57:
	In this theorem statement, we assume derivations whose ''inputs'' are related by an identity relation, and show that the outputs are identical as well. This theorem statement applies when we have evidence that the inputs are identical but the two derivations of the judgement in question have different types. The proof is no more complicated than the previous formulation, because when we derive the precondition <tt>id-bit B1 B1'</tt> using <tt>id-bit/refl</tt> (the only rule we could use to derive that fact), <tt>B1</tt> and <tt>B1'</tt> are forced to be identical objects, just as they were in the previous proof.		In this theorem statement, we assume derivations whose ''inputs'' are related by an identity relation, and show that the outputs are identical as well. This theorem statement applies when we have evidence that the inputs are identical but the two derivations of the judgement in question have different types. The proof is no more complicated than the previous formulation, because when we derive the precondition <tt>id-bit B1 B1'</tt> using <tt>id-bit/refl</tt> (the only rule we could use to derive that fact), <tt>B1</tt> and <tt>B1'</tt> are forced to be identical objects, just as they were in the previous proof.

-	<twelf check="true" ~~noinclude~~="true">	+	<twelf check="true" discard="true">
	bit-flip-unique-alt : id-bit B1 B1'		bit-flip-unique-alt : id-bit B1 B1'
	-> bit-flip B1 B2		-> bit-flip B1 B2
Line 71:		Line 71:
	%worlds () (bit-flip-unique-alt _ _ _ _).		%worlds () (bit-flip-unique-alt _ _ _ _).
	%total {} (bit-flip-unique-alt _ _ _ _).		%total {} (bit-flip-unique-alt _ _ _ _).
-	</twelf><twelf hidden="true" ~~include~~="alt">	+	</twelf><twelf hidden="true" import="alt">
	bit-flip-resp : id-bit B1 B1'		bit-flip-resp : id-bit B1 B1'
	-> id-bit B2 B2'		-> id-bit B2 B2'
Line 98:		Line 98:
	%total {} (bit-flip-unique-alt _ _ _ _).		%total {} (bit-flip-unique-alt _ _ _ _).
	</twelf>		</twelf>
-	However, this alternate formulation is equivalent to the above uniqueness lemma. It is easy to see that this lemma implies the above, as we can always call this lemma with <tt>id-bit/refl</tt>. To prove the other direction, we can compose the above uniqueness lemma with a [[respects lemma]] showing that <tt>bit-flip</tt> respects equality. <twelflink ~~include~~=alt>Here is an example</twelflink> of proving <tt>bit-flip-unique-alt</tt> using a uniqueness lemma and a respects lemma (<twelflink ~~include~~=alt check=true>here is Twelf's output</twelflink>). Because the [[respects lemma]] will often be necessary for other reasons, it is usually preferable to prove it and the above uniqueness lemma, rather than the composed version presented here.	+	However, this alternate formulation is equivalent to the above uniqueness lemma. It is easy to see that this lemma implies the above, as we can always call this lemma with <tt>id-bit/refl</tt>. To prove the other direction, we can compose the above uniqueness lemma with a [[respects lemma]] showing that <tt>bit-flip</tt> respects equality. <twelflink import=alt>Here is an example</twelflink> of proving <tt>bit-flip-unique-alt</tt> using a uniqueness lemma and a respects lemma (<twelflink import=alt check=true>here is Twelf's output</twelflink>). Because the [[respects lemma]] will often be necessary for other reasons, it is usually preferable to prove it and the above uniqueness lemma, rather than the composed version presented here.

	== Bigger example: determinism of evaluation ==		== Bigger example: determinism of evaluation ==

Totality assertion

2010-09-02T12:30:24Z

← Older revision		Revision as of 12:30, 2 September 2010
Line 9:		Line 9:
	Consider the following LF signature, which defined addition on natural numbers:		Consider the following LF signature, which defined addition on natural numbers:

-	<twelf ~~name="base"~~>	+	<twelf>
	nat : type.		nat : type.
	z : nat.		z : nat.

Tabled logic programming

2010-09-02T12:29:36Z

← Older revision		Revision as of 12:29, 2 September 2010
Line 94:		Line 94:
	<tt>a</tt> - ((<tt>b</tt> - ((<tt>a</tt> - <tt>b</tt> - <tt>d</tt>) - <tt>f</tt>))		<tt>a</tt> - ((<tt>b</tt> - ((<tt>a</tt> - <tt>b</tt> - <tt>d</tt>) - <tt>f</tt>))
	- <tt>g</tt>).		- <tt>g</tt>).
-	\|check=decl ~~noinclude~~=true}%	+	\|check=decl discard=true}%

	%querytabled * * D : path a g.		%querytabled * * D : path a g.
Line 101:		Line 101:
	We can also run a terminating search for a path that does not exist,		We can also run a terminating search for a path that does not exist,
	such as one from <tt>a</tt> to <tt>h</tt>.		such as one from <tt>a</tt> to <tt>h</tt>.
-	\|check=decl ~~noinclude~~=true}%	+	\|check=decl discard=true}%

	%querytabled * * D : path a h.		%querytabled * * D : path a h.

Substitution lemma

2010-09-02T12:27:51Z

← Older revision		Revision as of 12:27, 2 September 2010
Line 9:		Line 9:
	Consider the following encoding of a simply typed λ-calculus:		Consider the following encoding of a simply typed λ-calculus:

-	<twelf ~~group~~="application">	+	<twelf import="application">
	%% Syntax		%% Syntax

Line 40:		Line 40:
	We can give a direct proof of substitution:		We can give a direct proof of substitution:

-	<twelf ~~group~~="application" check="true">	+	<twelf import="application" check=true>
	subst : of E1 T		subst : of E1 T
	-> ({x:exp}{dx:of x T} of (E2 x) T')		-> ({x:exp}{dx:of x T} of (E2 x) T')
Line 72:		Line 72:

	Here is an encoding that uses a different judgement for assumptions:		Here is an encoding that uses a different judgement for assumptions:
-	<twelf ~~group~~="var">	+	<twelf import="var">
	%% Syntax		%% Syntax

Line 107:		Line 107:
	Now, we prove the substitution theorem:		Now, we prove the substitution theorem:

-	<twelf ~~group~~="var">	+	<twelf import="var">
	subst : of E1 T		subst : of E1 T
	-> ({x:exp}{dx:assm x T} of (E2 x) T')		-> ({x:exp}{dx:assm x T} of (E2 x) T')
Line 144:		Line 144:
	can be given as the second argument to the inductive call.		can be given as the second argument to the inductive call.

-	<twelf ~~group~~="var" check="true">	+	<twelf import="var" check=true>
	- : subst D1 ([x][dx] of/lam ([y][dy] D2 x dx y dy)) (of/lam D2')		- : subst D1 ([x][dx] of/lam ([y][dy] D2 x dx y dy)) (of/lam D2')
	<- ({y}{dy} subst D1 ([x][dx] D2 x dx y dy) (D2' y dy)).		<- ({y}{dy} subst D1 ([x][dx] D2 x dx y dy) (D2' y dy)).
Line 165:		Line 165:
	[[Explicit contexts]] could be used to do substition in this case, but this technique is much simpler in practice.		[[Explicit contexts]] could be used to do substition in this case, but this technique is much simpler in practice.

-	<twelf ~~group~~="depvar">tp : type.	+	<twelf import="depvar">tp : type.
	exp : type.		exp : type.

Line 209:		Line 209:
	The following metatheorem is actually true, but the naive attempt at proving it will fail.		The following metatheorem is actually true, but the naive attempt at proving it will fail.

-	<twelf ~~group~~="depvar">	+	<twelf import="depvar">
	subst-wontwork : of E1 T		subst-wontwork : of E1 T
	-> ({x:exp}{dx:assm x T} of (E2 x) (T' x))		-> ({x:exp}{dx:assm x T} of (E2 x) (T' x))
Line 234:		Line 234:
	The proof fails because this case is not general enough to cover all lambdas. Specifically, this case only applies if the type assigned to the variable y does not depend on the variable x.		The proof fails because this case is not general enough to cover all lambdas. Specifically, this case only applies if the type assigned to the variable y does not depend on the variable x.

-	<twelf ~~group~~="depvar">	+	<twelf import="depvar" check=decl discard=true>
	- : subst-wontwork D1 ([x][dx] of/lam ([y][dy:assm y T'] D2 x dx y dy)) (of/lam D2')		- : subst-wontwork D1 ([x][dx] of/lam ([y][dy:assm y T'] D2 x dx y dy)) (of/lam D2')
	<- ({y}{dy} subst-wontwork D1 ([x][dx] D2 x dx y dy) (D2' y dy)).		<- ({y}{dy} subst-wontwork D1 ([x][dx] D2 x dx y dy) (D2' y dy)).

	%worlds (assm-block) (subst-wontwork _ _ _).		%worlds (assm-block) (subst-wontwork _ _ _).
-	% %total (D1) (subst-wontwork _ D1 _).	+	%total (D1) (subst-wontwork _ D1 _).
	</twelf>		</twelf>

Line 251:		Line 251:
	are generalized by the schematic variables E3 and T'', respectively.		are generalized by the schematic variables E3 and T'', respectively.

-	<twelf ~~group~~="depvar">	+	<twelf import="depvar">
	subst* : of E1 T		subst* : of E1 T
	-> (assm E1 T -> of E3 T'')		-> (assm E1 T -> of E3 T'')
Line 282:		Line 282:
	Having proved the preceding lemma, the general substitution principle can be proven by first substituting E1 in for x, and then applying subst* to eliminate the dependency on assm E1 T.		Having proved the preceding lemma, the general substitution principle can be proven by first substituting E1 in for x, and then applying subst* to eliminate the dependency on assm E1 T.

-	<twelf ~~group~~="depvar" check="true">	+	<twelf import="depvar" check="true">
	subst : of E1 T		subst : of E1 T
	-> ({x:exp}{dx:assm x T} of (E2 x) (T' x))		-> ({x:exp}{dx:assm x T} of (E2 x) (T' x))

What's new

2010-09-02T12:13:28Z

spelling

← Older revision		Revision as of 12:13, 2 September 2010
Line 1:		Line 1:
	;September 1, 2010		;September 1, 2010
-	* The Twelf Wiki has undergone an upgrade, and in the process code underlying the syntax-highlighing [[TwelfTag]] system has been substantially rewritten and simplified. However, this meant several ~~depreciated~~-but-still-used options to the <nowiki><twelf></nowiki> tags now don't work and print error messages. Leave a note on [[User_talk:Rsimmons \| Rob's talk page]] if you see any weird error messages around Twelf code.	+	* The Twelf Wiki has undergone an upgrade, and in the process code underlying the syntax-highlighing [[TwelfTag]] system has been substantially rewritten and simplified. However, this meant several deprecated-but-still-used options to the <nowiki><twelf></nowiki> tags now don't work and print error messages. Leave a note on [[User_talk:Rsimmons \| Rob's talk page]] if you see any weird error messages around Twelf code.
	;February 22, 2009		;February 22, 2009
	* [[User:Rsimmons\|Rob]] has a case study on [[lax logic]] that uses the [[admissibility of cut]] and identity show a sound and complete correspondence between two sequent calculus presentations of lax logic.		* [[User:Rsimmons\|Rob]] has a case study on [[lax logic]] that uses the [[admissibility of cut]] and identity show a sound and complete correspondence between two sequent calculus presentations of lax logic.

User-defined constraint domain

2010-09-02T11:29:57Z

Show changes

%worlds

2010-09-02T01:33:57Z

edit fixing twelftag bug; also kill a useless twelftag

← Older revision		Revision as of 01:33, 2 September 2010
Line 30:		Line 30:
	The judgement <tt>max</tt> defined in this signature is a [[%total\|total]] relation on natural numbers, or LF terms of type <tt>nat</tt> in the empty LF context. We specify this totality assertion in Twelf with the following declarations:		The judgement <tt>max</tt> defined in this signature is a [[%total\|total]] relation on natural numbers, or LF terms of type <tt>nat</tt> in the empty LF context. We specify this totality assertion in Twelf with the following declarations:

-	<twelf check=true ~~name~~="maxtotal">	+	<twelf check=true export="maxtotal">
	%mode max +N1 +N2 -N3.		%mode max +N1 +N2 -N3.
	%worlds () (max _ _ _).		%worlds () (max _ _ _).
Line 44:		Line 44:
	The following <tt>[[%block]]</tt> declaration defines the block <tt>random_nat</tt>, which allows such variables:		The following <tt>[[%block]]</tt> declaration defines the block <tt>random_nat</tt>, which allows such variables:

-	<twelf ~~name~~=~~bad~~>	+	<twelf export="badnews">
	%block random_nat : block {x: nat}.		%block random_nat : block {x: nat}.

Line 53:		Line 53:
	If we attempt to verify the totality assertion for <tt>max</tt> in these worlds, Twelf reports an error: <tt>max</tt> is not defined in the "natural numbers" arising from LF variables in the context.		If we attempt to verify the totality assertion for <tt>max</tt> in these worlds, Twelf reports an error: <tt>max</tt> is not defined in the "natural numbers" arising from LF variables in the context.

-	<twelf ~~include~~=~~bad~~ check="decl">	+	<twelf import="badnews" check=decl>
	%total T (max T _ _).		%total T (max T _ _).
	</twelf>		</twelf>
Line 69:		Line 69:

	For example, consider the following signature for the lambda-calculus:		For example, consider the following signature for the lambda-calculus:
-	<twelf ~~include~~="maxtotal" ~~name~~="height">	+	<twelf import="maxtotal" export="height">
	exp : type.		exp : type.
	lam : (exp -> exp) -> exp.		lam : (exp -> exp) -> exp.
Line 76:		Line 76:

	We define a height relation on open lambda-terms as a [[hypothetical judgement]]; note that the height rule for variables is represented as an LF assumption:		We define a height relation on open lambda-terms as a [[hypothetical judgement]]; note that the height rule for variables is represented as an LF assumption:
-	<twelf ~~include~~="height">	+	<twelf import="height">
	height : exp -> nat -> type.		height : exp -> nat -> type.

Line 89:		Line 89:
	If we try to declare <tt>height</tt> to be defined in the closed world, as we did for <tt>max</tt>, Twelf will fail with a <tt>World violation</tt> [[error messages\|error message]]:		If we try to declare <tt>height</tt> to be defined in the closed world, as we did for <tt>max</tt>, Twelf will fail with a <tt>World violation</tt> [[error messages\|error message]]:

-	<twelf ~~include~~="height" discard="true" check="decl">	+	<twelf import="height" discard=true check=decl>
	%worlds () (height _ _).		%worlds () (height _ _).
	</twelf>		</twelf>
Line 99:		Line 99:
	The correct world for this type family consists of blocks of the form defined in the following <tt>[[%block]]</tt> declaration called <tt>var-height</tt>. These blocks specify that whenever a new variable with type <tt>exp</tt> is added to the context, it is added along with a derivation of <tt>height x (s z)</tt>. The type family <tt>height</tt> adequately represents the notion of height that we have in mind in this world. Moreover, it also world-checks in this world:		The correct world for this type family consists of blocks of the form defined in the following <tt>[[%block]]</tt> declaration called <tt>var-height</tt>. These blocks specify that whenever a new variable with type <tt>exp</tt> is added to the context, it is added along with a derivation of <tt>height x (s z)</tt>. The type family <tt>height</tt> adequately represents the notion of height that we have in mind in this world. Moreover, it also world-checks in this world:

-	<twelf ~~include~~="height" check="true">	+	<twelf import="height" check=true>
	%block var-height : block {x: exp}{_: height x (s z)}.		%block var-height : block {x: exp}{_: height x (s z)}.

Line 107:		Line 107:

	Indeed, the type family is total in this world as well:		Indeed, the type family is total in this world as well:
-	<twelf ~~include~~="height" check="decl">	+	<twelf import="height" check=decl>
	%total T (height T _).		%total T (height T _).
	</twelf>		</twelf>
-
-	~~You can <twelflink>see the code for this example</twelflink> or <twelflink check=true>see Twelf's output</twelflink >~~

	=== Subordination and world subsumption ===		=== Subordination and world subsumption ===

Implicit and explicit parameters

2010-09-02T01:29:06Z

← Older revision		Revision as of 01:29, 2 September 2010
(One intermediate revision not shown)
Line 11:		Line 11:
	=== Implicit parameters ===		=== Implicit parameters ===

-	<twelf hidden="true">	+	<twelf hidden=true>

	exp : type.		exp : type.
Line 24:		Line 24:
	of0 : of 0 bit.		of0 : of 0 bit.

-	</twelf><twelf ~~noinclude~~="true" check="decl">	+	</twelf><twelf discard=true check=decl>

	translate-i : of M A -> of M' A -> type.		translate-i : of M A -> of M' A -> type.
Line 35:		Line 35:
	Note that in this example we use slightly bad [[style guide\|style]], capitalizing our bound variables <tt>M</tt>, <tt>A</tt>, and <tt>M'</tt>.		Note that in this example we use slightly bad [[style guide\|style]], capitalizing our bound variables <tt>M</tt>, <tt>A</tt>, and <tt>M'</tt>.

-	<twelf ~~noinclude~~="true" check="decl">	+	<twelf discard=true check=decl>

Equality

2010-09-02T01:27:49Z

← Older revision		Revision as of 01:27, 2 September 2010
Line 2:		Line 2:

	One such circumstance is when we wish to prove a [[uniqueness lemma]] showing that an object-language judgement determines some outputs uniquely. For example, consider the [[Proving metatheorems:Representing the judgements of the natural numbers\|addition judgement on natural numbers]]. To state this uniqueness lemma, we must define a judgement <tt>eq N N'</tt> representing equality of natural numbers. Then the theorem is stated as follows:		One such circumstance is when we wish to prove a [[uniqueness lemma]] showing that an object-language judgement determines some outputs uniquely. For example, consider the [[Proving metatheorems:Representing the judgements of the natural numbers\|addition judgement on natural numbers]]. To state this uniqueness lemma, we must define a judgement <tt>eq N N'</tt> representing equality of natural numbers. Then the theorem is stated as follows:
-	<twelf ~~noinclude~~=true>	+	<twelf discard=true>
	plus-unique : plus N1 N2 N3		plus-unique : plus N1 N2 N3
	-> plus N1 N2 N3'		-> plus N1 N2 N3'
Line 84:		Line 84:

	* Other relations respect equality, in the sense that we can replace equals for equals. For example, if we have a height relation on trees, then we will be able to prove the following metatheorem:		* Other relations respect equality, in the sense that we can replace equals for equals. For example, if we have a height relation on trees, then we will be able to prove the following metatheorem:
-	<twelf hidden="true">nat : type.</twelf>	+	<twelf hidden=true>nat : type.</twelf>
	<twelf>		<twelf>
	height : tree -> nat -> type.		height : tree -> nat -> type.
Line 161:		Line 161:
	Properties analogous to before are admissible, but the theorems for <tt>tree</tt> will have premises referring to <tt>id-nat</tt>. For example:		Properties analogous to before are admissible, but the theorems for <tt>tree</tt> will have premises referring to <tt>id-nat</tt>. For example:

-	<twelf check="true">	+	<twelf check=true>
	id-tree-node-cong : id-tree T1 T1'		id-tree-node-cong : id-tree T1 T1'
	-> id-tree T2 T2'		-> id-tree T2 T2'

Effectiveness lemma

2010-09-01T21:48:37Z

Fix twelftag bugs

← Older revision		Revision as of 21:48, 1 September 2010
Line 81:		Line 81:
	For simplicity, assume the language is manifestly terminating, so the progress theorem can be proved by a simple inductive argument that shows that all terms evaluate to a value:		For simplicity, assume the language is manifestly terminating, so the progress theorem can be proved by a simple inductive argument that shows that all terms evaluate to a value:

-	<twelf ~~name~~=_>	+	<twelf discard=true>
	progress : of E T -> eval E V -> type.		progress : of E T -> eval E V -> type.
	%mode progress +D1 -D2.		%mode progress +D1 -D2.
	%worlds () (progress _ _).		%worlds () (progress _ _).
	</twelf>		</twelf>
-	<twelf hidden="true">	+	<twelf hidden=true>
	progress : of E T -> eval E V -> type.		progress : of E T -> eval E V -> type.
	%mode progress +D1 -D2.		%mode progress +D1 -D2.
Line 93:		Line 93:
	Now, consider the case of progress for <tt>of-neg</tt>:		Now, consider the case of progress for <tt>of-neg</tt>:

-	<twelf check="decl~~" name~~=~~"_"~~>	+	<twelf check=decl discard=true>
	- : {Dflip : bit-flip B B'}		- : {Dflip : bit-flip B B'}
	progress		progress
Line 109:		Line 109:
	The work-around is to prove the effectiveness lemma. Using the above effectiveness lemma, we can finish this case as follows:		The work-around is to prove the effectiveness lemma. Using the above effectiveness lemma, we can finish this case as follows:

-	<twelf check="decl">	+	<twelf check=decl>
	- : progress		- : progress
	(of-neg (Dof : of E tp/bit))		(of-neg (Dof : of E tp/bit))

Coverage checking

2010-09-01T21:47:27Z

Fix twelftag bugs

← Older revision		Revision as of 21:47, 1 September 2010
Line 7:		Line 7:
	We will use the common example of [[natural numbers]] for this example:		We will use the common example of [[natural numbers]] for this example:

-	<twelf ~~name~~=nat>	+	<twelf import="nat">
	nat: type.		nat: type.

Line 19:		Line 19:
	Input coverage is similar to exhaustiveness checking in ML, in that it ensures that your relation is prepared to accept any input that is thrown at it. We would run afoul of the input coverage checker if we tried to run a <tt>%covers</tt> or <tt>%total</tt> declaration on the relation <tt>half</tt> that halves a natural number but is undefined on odd numbers. Another example of input coverage checking can be seen at the page on <tt>[[%covers]]</tt>.		Input coverage is similar to exhaustiveness checking in ML, in that it ensures that your relation is prepared to accept any input that is thrown at it. We would run afoul of the input coverage checker if we tried to run a <tt>%covers</tt> or <tt>%total</tt> declaration on the relation <tt>half</tt> that halves a natural number but is undefined on odd numbers. Another example of input coverage checking can be seen at the page on <tt>[[%covers]]</tt>.

-	<twelf ~~include~~=nat ~~name~~=one>	+	<twelf import="nat" export="one">
	half : nat -> nat -> type.		half : nat -> nat -> type.
	%mode half +N1 -N2.		%mode half +N1 -N2.
Line 30:		Line 30:
	</twelf>		</twelf>

-	<twelf ~~include~~=one ~~name="_~~" check=decl>	+	<twelf import="one" check=decl discard=true>
	%total N (half N _).		%total N (half N _).
	</twelf>		</twelf>
Line 42:		Line 42:
	Say we attempted to fix <tt>half</tt> by defining <tt>half</tt> of 1 to be 0 by adding the case <tt>half/1</tt> shown below:		Say we attempted to fix <tt>half</tt> by defining <tt>half</tt> of 1 to be 0 by adding the case <tt>half/1</tt> shown below:

-	<twelf ~~include~~=nat ~~name~~=two>	+	<twelf import="nat" export="two">
	half : nat -> nat -> type.		half : nat -> nat -> type.
	%mode half +N1 -N2.		%mode half +N1 -N2.
Line 57:		Line 57:
	For pedagogical purposes, we have given the constant <tt>half/1</tt> an unnecessary extra premise that <tt>half z z </tt>. Thus, the case <tt>half/1</tt> expects the "output" of the subgoal <tt><- half z z</tt> to be <tt>z</tt>; inspecting the program, this is a true fact, but Twelf is not capable of verifying this and complains accordingly.		For pedagogical purposes, we have given the constant <tt>half/1</tt> an unnecessary extra premise that <tt>half z z </tt>. Thus, the case <tt>half/1</tt> expects the "output" of the subgoal <tt><- half z z</tt> to be <tt>z</tt>; inspecting the program, this is a true fact, but Twelf is not capable of verifying this and complains accordingly.

-	<twelf ~~include~~=two check=decl>	+	<twelf import="two" check=decl>
	%total N (half N _).		%total N (half N _).
	</twelf>		</twelf>
Line 63:		Line 63:
	In this case, we can fix the problem in one of two ways. First, we can remove the subgoal entirely:		In this case, we can fix the problem in one of two ways. First, we can remove the subgoal entirely:

-	<twelf ~~name~~=~~"_"~~>	+	<twelf discard=true>
	half/1 : half (s z) z.		half/1 : half (s z) z.
	</twelf>		</twelf>
Line 69:		Line 69:
	Alternatively, we can rewrite the subgoal, leaving the output a free variable:		Alternatively, we can rewrite the subgoal, leaving the output a free variable:

-	<twelf ~~name~~=~~"_"~~>	+	<twelf discard=true>
	half/1 : half (s z) N		half/1 : half (s z) N
	<- half z N.		<- half z N.

Constraint domain

2010-09-01T21:45:57Z

Fix twelftag bugs

← Older revision		Revision as of 21:45, 1 September 2010
Line 7:		Line 7:
	The rational numbers with equality add a new type family, <tt>rational</tt>, and operators for rational addition, subtraction, multiplication, and negation.		The rational numbers with equality add a new type family, <tt>rational</tt>, and operators for rational addition, subtraction, multiplication, and negation.

-	<twelf ~~include~~="er" check="decl">	+	<twelf import="er" check=decl>
	%use equality/rationals.		%use equality/rationals.
	</twelf>		</twelf>

	The rational numbers are automatically simplified by Twelf		The rational numbers are automatically simplified by Twelf
-	<twelf ~~check~~="~~decl~~" ~~include~~=~~"er"~~>	+	<twelf import="er" check=decl>
	mynum = 1/4 + ~ 9/2.		mynum = 1/4 + ~ 9/2.
	</twelf>		</twelf>
Line 18:		Line 18:
	Because of this automatic simplification, equality is not actually added by the <tt>%use</tt> declaration, becuase it can be introduced the same way [[identity]] is introduced for any other type family in Twelf.		Because of this automatic simplification, equality is not actually added by the <tt>%use</tt> declaration, becuase it can be introduced the same way [[identity]] is introduced for any other type family in Twelf.

-	<twelf ~~include~~="er">	+	<twelf import="er">
	eq : rational -> rational -> type.		eq : rational -> rational -> type.
	eq/is : eq X X.		eq/is : eq X X.
Line 30:		Line 30:
	This declaration introduces everything introduced by <tt>%use equality/rationals</tt>, as well as ways to check for		This declaration introduces everything introduced by <tt>%use equality/rationals</tt>, as well as ways to check for

-	<twelf ~~include~~="ir" check="decl">	+	<twelf import="ir" check=decl>
	%use inequality/rationals.		%use inequality/rationals.
	</twelf>		</twelf>
Line 36:		Line 36:
	Inequality relations can be used like normal goals, as they are in the next example, even though the User's Guide explains that their internal behavior is different than other goals.		Inequality relations can be used like normal goals, as they are in the next example, even though the User's Guide explains that their internal behavior is different than other goals.

-	<twelf ~~include~~="ir" check="true">	+	<twelf import="ir" check=true>
	more-than-two : rational -> rational -> type.		more-than-two : rational -> rational -> type.
	more-than-two/i : more-than-two R1 R2		more-than-two/i : more-than-two R1 R2
Line 49:		Line 49:
	The introduction of integers with equality looks similar to the introduction of rationals with equality, but with a different type family, <tt>integer</tt>.		The introduction of integers with equality looks similar to the introduction of rationals with equality, but with a different type family, <tt>integer</tt>.

-	<twelf ~~include~~="ie" check="decl">	+	<twelf import="ie" check=decl>
	%use equality/integers.		%use equality/integers.
	</twelf>		</twelf>
Line 60:		Line 60:
	The introduction of integers with inequality is a good bit shorter than the introduction of rationals with inequality, because Twelf can take advantage of the facts like <tt>X + 1 > Y</tt> iff <tt>X >= Y</tt>.		The introduction of integers with inequality is a good bit shorter than the introduction of rationals with inequality, because Twelf can take advantage of the facts like <tt>X + 1 > Y</tt> iff <tt>X >= Y</tt>.

-	<twelf ~~include~~="ii" check="decl">	+	<twelf import="ii" check=decl>
	%use inequality/integers.		%use inequality/integers.
	</twelf>		</twelf>
Line 71:		Line 71:
	This constraint domain allows Twelf to include strings of characters.		This constraint domain allows Twelf to include strings of characters.

-	<twelf ~~include~~="str" check="decl">	+	<twelf import="str" check=decl>
	%use equality/strings.		%use equality/strings.
	</twelf>		</twelf>
Line 77:		Line 77:
	Like the other constriant domains, using the operators automatically simplifies the operators away. The only one provided is concatenation, <tt>++</tt>, which is shown below:		Like the other constriant domains, using the operators automatically simplifies the operators away. The only one provided is concatenation, <tt>++</tt>, which is shown below:

-	<twelf ~~include~~="str" check="decl">	+	<twelf import="str" check=decl>
	mystring = "Hello" ++ " " ++ "World" ++ "!".		mystring = "Hello" ++ " " ++ "World" ++ "!".
	</twelf>		</twelf>
Line 88:		Line 88:
	The <tt>word32</tt> extension behaves very differently than the others - operators are relations, not functions, and so Twelf does not simplify their application away.		The <tt>word32</tt> extension behaves very differently than the others - operators are relations, not functions, and so Twelf does not simplify their application away.

-	<twelf ~~include~~="w32" check="decl">	+	<twelf import="w32" check=decl>
	%use word32.		%use word32.
	</twelf>		</twelf>
Line 94:		Line 94:
	Behind the scenes, using the <tt>word32</tt> extension adds axioms to the signature like <tt>3+15</tt> shown in the below example. The <tt>prove+</tt> relations that are defined act like [[effectiveness lemmas]] for these relations.		Behind the scenes, using the <tt>word32</tt> extension adds axioms to the signature like <tt>3+15</tt> shown in the below example. The <tt>prove+</tt> relations that are defined act like [[effectiveness lemmas]] for these relations.

-	<twelf ~~check~~="~~decl~~" ~~include~~=~~"w32"~~>	+	<twelf import="w32" check=decl>
	myproof = 3+15.		myproof = 3+15.

Canonical forms lemma

2010-09-01T21:43:17Z

Fix twelftag bugs

← Older revision		Revision as of 21:43, 1 September 2010
Line 11:		Line 11:
	Consider the following language:		Consider the following language:

-	<twelf ~~name~~="free-judgements">	+	<twelf import="free-judgements">
	tp : type.		tp : type.
	tp/unit : tp.		tp/unit : tp.
Line 66:		Line 66:
	To prove progress for this language, we use an [[output factoring]] lemma that collects the post-inductive-call reasoning in the application case:		To prove progress for this language, we use an [[output factoring]] lemma that collects the post-inductive-call reasoning in the application case:

-	<twelf ~~name~~="free" ~~include~~="free-judgements">	+	<twelf export="free" import="free-judgements">
	progress-exp/app : notstuck E1		progress-exp/app : notstuck E1
	-> notstuck E2		-> notstuck E2
Line 90:		Line 90:

	It is then simple to complete the proof of progress:		It is then simple to complete the proof of progress:
-	<twelf ~~include~~="free" check="true">	+	<twelf import="free" check=true>
	progress : of E T		progress : of E T
	-> notstuck E		-> notstuck E
Line 115:		Line 115:
	For example, we extend the above language with a trivial notion of subtyping. It is equivalent to syntactic equality on types. The purpose of this tutorial is to illustrate how to state/prove canonical forms lemmas when subtyping/equality are part of the type system, and this trivial notion is enough to motivate the discussion.		For example, we extend the above language with a trivial notion of subtyping. It is equivalent to syntactic equality on types. The purpose of this tutorial is to illustrate how to state/prove canonical forms lemmas when subtyping/equality are part of the type system, and this trivial notion is enough to motivate the discussion.

-	<twelf ~~name~~="~~equality~~-judgements" ~~include~~="~~free~~-judgements">	+	<twelf import="free-judgements" export="equality-judgements">
	tp-sub : tp -> tp -> type.		tp-sub : tp -> tp -> type.

Line 131:		Line 131:
	Now, we state and prove the canonical forms lemma explicitly. In the theorem statement, we use the syntactic equality judgement as an output in order to state "E1 is of the form (exp/lam T E)".		Now, we state and prove the canonical forms lemma explicitly. In the theorem statement, we use the syntactic equality judgement as an output in order to state "E1 is of the form (exp/lam T E)".

-	<twelf ~~name~~="equality" ~~include~~="equality~~-judgements~~">	+	<twelf import="equality-judgements" export="equality">
	seq-exp : exp -> exp -> type.		seq-exp : exp -> exp -> type.
	seq-exp/i : seq-exp E E.		seq-exp/i : seq-exp E E.
Line 152:		Line 152:
	Next, we define a helper lemma for showing that (exp/app E1 E2) is notstuck when E1 is of the form (exp/lam T E) and E2 is a value. We use this lemma because we get the derivation of (seq-exp E1 (exp/lam T E)) as the output of the canonical forms lemma. If we were to try to invert the derivation as an output, we would cause Twelf's coverage checker to fail. So instead, we call a helper lemma with the equality derivation as an input. Because the derivation is an input, we can safely apply inversion on it.		Next, we define a helper lemma for showing that (exp/app E1 E2) is notstuck when E1 is of the form (exp/lam T E) and E2 is a value. We use this lemma because we get the derivation of (seq-exp E1 (exp/lam T E)) as the output of the canonical forms lemma. If we were to try to invert the derivation as an output, we would cause Twelf's coverage checker to fail. So instead, we call a helper lemma with the equality derivation as an input. Because the derivation is an input, we can safely apply inversion on it.

-	<twelf ~~include~~="equality">	+	<twelf import="equality">
	progress-exp/app-beta : seq-exp E1 (exp/lam T E)		progress-exp/app-beta : seq-exp E1 (exp/lam T E)
	-> val E2		-> val E2
Line 167:		Line 167:
	Next, we prove the output factoring lemma:		Next, we prove the output factoring lemma:

-	<twelf ~~include~~="equality">	+	<twelf import="equality">
	progress-exp/app : notstuck E1		progress-exp/app : notstuck E1
	-> notstuck E2		-> notstuck E2
Line 184:		Line 184:
	Because there is more than one way to derive that a value that has an arrow type, we must use the canonical forms lemma we have just proven. To make use of the equality we get out of the canonical forms lemma, we call the special helper lemma progress-exp/app-beta.		Because there is more than one way to derive that a value that has an arrow type, we must use the canonical forms lemma we have just proven. To make use of the equality we get out of the canonical forms lemma, we call the special helper lemma progress-exp/app-beta.

-	<twelf ~~include~~="equality" check="true">	+	<twelf import="equality" check=true>
	- : progress-exp/app (notstuck/val V) (notstuck/val V2) D1		- : progress-exp/app (notstuck/val V) (notstuck/val V2) D1
	NS		NS
Line 196:		Line 196:
	Finally, we prove the overall progress theorem as before.		Finally, we prove the overall progress theorem as before.

-	<twelf ~~include~~="equality" check="true">	+	<twelf import="equality" check=true>
	progress : of E T		progress : of E T
	-> notstuck E		-> notstuck E

%query

2010-09-01T21:15:15Z

← Older revision		Revision as of 21:15, 1 September 2010
Line 35:		Line 35:
	</twelf>		</twelf>

-	<twelf ~~noinclude~~=true check=true>	+	<twelf discard=true check=true>
	%query 1 * member d sample-list. % There is exactly one "d" in the list		%query 1 * member d sample-list. % There is exactly one "d" in the list
	%query 3 3 member a sample-list. % There are at least three "a's" in the list		%query 3 3 member a sample-list. % There are at least three "a's" in the list

%name

2010-09-01T20:08:50Z

tag fixes

← Older revision		Revision as of 20:08, 1 September 2010
Line 47:		Line 47:
	We can also use the <tt>%name</tt> declaration to define the default name for bound variables.		We can also use the <tt>%name</tt> declaration to define the default name for bound variables.

-	<twelf ~~include~~="lam">	+	<twelf import="lam">
	exp : type.		exp : type.

Line 65:		Line 65:
	The default prefix for universally quantified variables is again <tt>X</tt>. Also, observe that the default prefix for bound variables is <tt>x</tt>.		The default prefix for universally quantified variables is again <tt>X</tt>. Also, observe that the default prefix for bound variables is <tt>x</tt>.

-	<twelf ~~include~~="lam" check="decl">	+	<twelf import="lam" check=decl>
	_ = (step/app (step/app step/appabs)).		_ = (step/app (step/app step/appabs)).
	</twelf>		</twelf>
Line 72:		Line 72:
	This <tt>%name</tt> declaration causes no output from Twelf, but it changes the prefixes of universally quantified and bound variables to <tt>E</tt> and <tt>e</tt>, respectively.		This <tt>%name</tt> declaration causes no output from Twelf, but it changes the prefixes of universally quantified and bound variables to <tt>E</tt> and <tt>e</tt>, respectively.

-	<twelf ~~include~~="lam" check="decl">	+	<twelf import="lam" check=decl>
	%name exp E e.		%name exp E e.

%mode

2010-09-01T20:07:47Z

← Older revision		Revision as of 20:07, 1 September 2010
Line 11:		Line 11:
	Each argument <tt>ai</tt> is <tt>+</tt>''ID'', <tt>-</tt>''ID'', or <tt></tt>''ID'' for some distinct identifier ''ID''. <tt>+</tt> indicates that the argument is an input, <tt>-</tt> that it is an output, and <tt></tt> that the argument is unrestricted. (The <tt>*</tt> mode is rarely used.) For example, a natural mode for the <tt>plus</tt> relation on [[natural numbers]] is:		Each argument <tt>ai</tt> is <tt>+</tt>''ID'', <tt>-</tt>''ID'', or <tt></tt>''ID'' for some distinct identifier ''ID''. <tt>+</tt> indicates that the argument is an input, <tt>-</tt> that it is an output, and <tt></tt> that the argument is unrestricted. (The <tt>*</tt> mode is rarely used.) For example, a natural mode for the <tt>plus</tt> relation on [[natural numbers]] is:

-	<twelf ~~name~~=~~"_"~~>	+	<twelf discard=true>
	plus : nat -> nat -> nat -> type.		plus : nat -> nat -> nat -> type.
	%mode plus +N1 +N2 -N3.		%mode plus +N1 +N2 -N3.
Line 22:		Line 22:
	The short mode declaration above only specifies the mode for explicit parameters; the modes for implicit parameters are then assigned automatically. Occasionally, one needs to use a "full" form to specify the modes of implicit parameters:		The short mode declaration above only specifies the mode for explicit parameters; the modes for implicit parameters are then assigned automatically. Occasionally, one needs to use a "full" form to specify the modes of implicit parameters:

-	<twelf ~~name~~=~~"_"~~>	+	<twelf discard=true>
	%mode p1 ... pm term.		%mode p1 ... pm term.
	</twelf>		</twelf>
Line 28:		Line 28:
	Each parameter <tt>pi</tt> is <tt>+{</tt>''ID''<tt> : term}</tt>, <tt>-{</tt>''ID''<tt> : term}</tt>, or <tt>*{</tt>''ID''<tt> : term}</tt> for distinct identifiers ''ID''. Terms may refer to the variables bound in the previous parameters. For example, the full mode declaration corresponding to the short one above would be:		Each parameter <tt>pi</tt> is <tt>+{</tt>''ID''<tt> : term}</tt>, <tt>-{</tt>''ID''<tt> : term}</tt>, or <tt>*{</tt>''ID''<tt> : term}</tt> for distinct identifiers ''ID''. Terms may refer to the variables bound in the previous parameters. For example, the full mode declaration corresponding to the short one above would be:

-	<twelf ~~name~~=~~"_"~~>	+	<twelf discard=true>
	plus : nat -> nat -> nat -> type.		plus : nat -> nat -> nat -> type.
	%mode +{N1:nat} +{N2:nat} -{N3:nat} plus N1 N2 N3.		%mode +{N1:nat} +{N2:nat} -{N3:nat} plus N1 N2 N3.

%freeze

2010-09-01T20:06:27Z

← Older revision		Revision as of 20:06, 1 September 2010
(One intermediate revision not shown)
Line 16:		Line 16:
	<twelf>		<twelf>
	nat : type.		nat : type.
-	z : nat.	+	z : nat.
	s : nat -> nat. %prefix 9999 s.		s : nat -> nat. %prefix 9999 s.

Line 29:		Line 29:
	At this point, we may still extend the definition of addition:		At this point, we may still extend the definition of addition:

-	<twelf check="decl">	+	<twelf check=decl>
	plus/zz : plus M z M.		plus/zz : plus M z M.
	</twelf>		</twelf>
Line 35:		Line 35:
	However, if we freeze <tt>plus</tt> then this will not be allowed:		However, if we freeze <tt>plus</tt> then this will not be allowed:

-	<twelf check="decl~~" name~~=~~"fp"~~>	+	<twelf check=decl discard=true>
	%freeze plus.		%freeze plus.
	plus/zzz : plus z z z.		plus/zzz : plus z z z.
Line 42:		Line 42:
	More subtly, we will not be able to extend the [[subordination]] relation for <tt>plus</tt>:		More subtly, we will not be able to extend the [[subordination]] relation for <tt>plus</tt>:

-	<twelf check="decl~~" name~~=~~"fp2"~~>	+	<twelf check=decl discard=true>
	%freeze plus.		%freeze plus.
	thing : type.		thing : type.
Line 51:		Line 51:
	The subordination relation can be extended such that other non-frozen types depend on a frozen type, of course:		The subordination relation can be extended such that other non-frozen types depend on a frozen type, of course:

-	<twelf check="decl~~" name~~=~~"fp3"~~>	+	<twelf check=decl discard=true>
	%freeze plus.		%freeze plus.
	thing : type.		thing : type.

Deterministic declaration

2010-09-01T19:42:11Z

updates

← Older revision		Revision as of 19:42, 1 September 2010
Line 34:		Line 34:
	If <tt>findlabel</tt> is not declared deterministic, all four solutions can be returned, but with <tt>findlabel</tt> declared deterministic only one will be found.		If <tt>findlabel</tt> is not declared deterministic, all four solutions can be returned, but with <tt>findlabel</tt> declared deterministic only one will be found.

-	<twelf check=decl ~~noinclude~~=true>	+	<twelf check=decl discard=true>
	%query 4 * findlabel testtree L.		%query 4 * findlabel testtree L.
	</twelf>		</twelf>

-	<twelf check=decl ~~noinclude~~=true>	+	<twelf check=decl discard=true>
	%deterministic findlabel.		%deterministic findlabel.
	%query 1 * findlabel testtree L.		%query 1 * findlabel testtree L.
Line 60:		Line 60:
	Using <tt>searchfor</tt> to look for <tt>c</tt> in our test tree will cause backtracking, because <tt>findlabel</tt> first make <tt>L'<tt> equal to <tt>a</tt>, then <tt>b</tt>, then <tt>c</tt>.		Using <tt>searchfor</tt> to look for <tt>c</tt> in our test tree will cause backtracking, because <tt>findlabel</tt> first make <tt>L'<tt> equal to <tt>a</tt>, then <tt>b</tt>, then <tt>c</tt>.

-	<twelf check=decl ~~noinclude~~=true>	+	<twelf check=decl discard=true>
	%query 1 * P : searchfor testtree c.		%query 1 * P : searchfor testtree c.
	</twelf>		</twelf>
Line 66:		Line 66:
	If <tt>findlabel</tt> is deterministic, then the same search will make <tt>L'</tt> equal <tt>a</tt>, and will then be unable to backtrack.		If <tt>findlabel</tt> is deterministic, then the same search will make <tt>L'</tt> equal <tt>a</tt>, and will then be unable to backtrack.

-	<twelf check=decl ~~noinclude~~=true>	+	<twelf check=decl discard=true>
	%deterministic findlabel.		%deterministic findlabel.
	%query 1 * P : searchfor testtree c.		%query 1 * P : searchfor testtree c.

POPL Tutorial/Basic error messages

2010-09-01T18:30:48Z

Fix twelftag bugs

← Older revision		Revision as of 18:30, 1 September 2010
(2 intermediate revisions not shown)
Line 10:		Line 10:
	We'll start from the following code:		We'll start from the following code:

-	<twelf ~~name~~="base">	+	<twelf import="base">
	nat : type.		nat : type.
	zero : nat.		zero : nat.
Line 26:		Line 26:
	</twelf>		</twelf>

-	<twelf ~~name~~="m" ~~include~~="~~base~~">	+	<twelf import="base" export="mult">
	mult : nat -> nat -> nat -> type.		mult : nat -> nat -> nat -> type.
	%mode mult +M +N -P.		%mode mult +M +N -P.
Line 35:		Line 35:
	<- add N P P'.		<- add N P P'.
	</twelf>		</twelf>
-

	===Mode===		===Mode===
Line 46:		Line 45:
	determine the outputs of the conclusion.		determine the outputs of the conclusion.
	For example, the constant		For example, the constant
-	<twelf ~~name~~="~~examplesucc~~" ~~ignore~~="true">	+	<twelf import="mult" discard=true>
	mult/s : mult (succ M) N P'		mult/s : mult (succ M) N P'
	<- mult M N P		<- mult M N P
Line 58:		Line 57:
	On the other hand, a constant		On the other hand, a constant

-	<twelf ~~include~~="~~m" name="badmode~~" check="decl">	+	<twelf import="mult" check=decl discard=true>
	mult/bad-mode-output : mult zero N P.		mult/bad-mode-output : mult zero N P.
	</twelf>		</twelf>
	is not well-moded---the output <tt>P</tt> is not determined by the		is not well-moded---the output <tt>P</tt> is not determined by the
	inputs. Similarly,		inputs. Similarly,
-	<twelf ~~include~~="~~m" name="badmode2~~" check="decl">	+	<twelf import="mult" check=decl discard=true>
	mult/bad-mode-input : mult (succ M) N zero		mult/bad-mode-input : mult (succ M) N zero
	<- mult M Q P.		<- mult M Q P.
Line 72:		Line 71:
	Note that subgoal order matters:		Note that subgoal order matters:

-	<twelf ~~include~~="~~m" name="subgoal~~" check="decl">	+	<twelf import="mult" check=decl discard=true>
	mult/s : mult (succ M) N Q		mult/s : mult (succ M) N Q
	<- add P N Q		<- add P N Q
Line 79:		Line 78:

	The premises are mode-checked in order; the outputs from one subgoal are		The premises are mode-checked in order; the outputs from one subgoal are
-	consider ground in subsequent premises.	+	consider ground in subsequent premises.

	===Worlds===		===Worlds===
Line 96:		Line 95:
	For example, the constant		For example, the constant

-	<twelf ~~name~~="~~termination~~" ~~ignore~~="true">	+	<twelf import="mult" discard=true>
	mult/s : mult (s M) N Q		mult/s : mult (s M) N Q
	<- mult M N P		<- mult M N P
Line 106:		Line 105:

	Recuring on exactly the same term is obviously a termination error:		Recuring on exactly the same term is obviously a termination error:
-	<twelf ~~include~~="~~m" name="termination1~~" check="decl">	+	<twelf import="mult" check=decl discard=true>
	mult/bad-termination-1 : mult M N P		mult/bad-termination-1 : mult M N P
	<- mult M N P.		<- mult M N P.
Line 114:		Line 113:
	As is recuring on an entirely unrelated argumenet:		As is recuring on an entirely unrelated argumenet:

-	<twelf ~~include~~="~~m" name="termination1~~" check="decl">	+	<twelf import="mult" check=decl discard=true>
	mult/bad-termination-2 : mult M N P		mult/bad-termination-2 : mult M N P
	<- mult N N P.		<- mult N N P.
Line 124:		Line 123:
	<tt>N</tt> in the conclusion of this constant appears in the premise:		<tt>N</tt> in the conclusion of this constant appears in the premise:

-	<twelf ~~include~~="~~m" name="badtotal~~" check="decl">	+	<twelf import="mult" check=decl discard=true>
	%total N (mult _ N _).		%total N (mult _ N _).
	</twelf>		</twelf>
Line 135:		Line 134:
	In the definition of a type family, you may pattern-match the outputs of		In the definition of a type family, you may pattern-match the outputs of
	a premise. For example, we might write		a premise. For example, we might write
-	<twelf ~~include~~="~~m" name="badoutput~~" check="decl">	+	<twelf import="mult" check=decl discard=true>
	mult/bad-output-cov : mult (succ M) N zero		mult/bad-output-cov : mult (succ M) N zero
	<- mult M N (succ P).		<- mult M N (succ P).
Line 160:		Line 159:
	For example:		For example:

-	<twelf ~~include~~="~~m" name="badoutputfreeness~~" check="decl">	+	<twelf import="mult" check=decl discard=true>
	mult/bad-output-free : mult (succ M) N zero		mult/bad-output-free : mult (succ M) N zero
	<- mult M N N.		<- mult M N N.
Line 186:		Line 185:
	<tt>mult</tt> would fail. For example:		<tt>mult</tt> would fail. For example:

-	<twelf ~~include~~="base~~" name="inputcov~~" check="decl">	+	<twelf import="base" check=decl discard=true>
	mult' : nat -> nat -> nat -> type.		mult' : nat -> nat -> nat -> type.
	%mode mult' +N1 +N2 -X3.		%mode mult' +N1 +N2 -X3.

Hereditary substitution for the STLC

2010-09-01T16:36:19Z

Hereditary substitution:

← Older revision		Revision as of 16:36, 1 September 2010
Line 116:		Line 116:
	The head variable of an atomic term <tt>R</tt> is the variable at the root of a series of eliminations. E.g., the head of <tt>fst (app x c)</tt> is <tt>x</tt>. When a canonical form is substituted for a head variable, hereditary substitution continues reducing. E.g., the following judgement is derivable:		The head variable of an atomic term <tt>R</tt> is the variable at the root of a series of eliminations. E.g., the head of <tt>fst (app x c)</tt> is <tt>x</tt>. When a canonical form is substituted for a head variable, hereditary substitution continues reducing. E.g., the following judgement is derivable:

-	<twelf ~~name~~=~~"_"~~>	+	<twelf discard=true>
	hsubst_rr		hsubst_rr
	(lam ([x] (pair c c)))		(lam ([x] (pair c c)))

Bracket abstraction

2010-09-01T16:01:52Z

← Older revision		Revision as of 16:01, 1 September 2010
Line 45:		Line 45:
	single-step reduction relation on combinator terms.		single-step reduction relation on combinator terms.
	}%		}%
-		+
	step : term -> term -> type.		step : term -> term -> type.

What's new

2010-09-01T15:31:27Z

reword that

← Older revision		Revision as of 15:31, 1 September 2010
(One intermediate revision not shown)
Line 1:		Line 1:
		+	;September 1, 2010
		+	* The Twelf Wiki has undergone an upgrade, and in the process code underlying the syntax-highlighing [[TwelfTag]] system has been substantially rewritten and simplified. However, this meant several depreciated-but-still-used options to the <nowiki><twelf></nowiki> tags now don't work and print error messages. Leave a note on [[User_talk:Rsimmons \| Rob's talk page]] if you see any weird error messages around Twelf code.
	;February 22, 2009		;February 22, 2009
	* [[User:Rsimmons\|Rob]] has a case study on [[lax logic]] that uses the [[admissibility of cut]] and identity show a sound and complete correspondence between two sequent calculus presentations of lax logic.		* [[User:Rsimmons\|Rob]] has a case study on [[lax logic]] that uses the [[admissibility of cut]] and identity show a sound and complete correspondence between two sequent calculus presentations of lax logic.

The Twelf Project:TwelfTag

2010-09-01T15:22:19Z

The check=decl option:

Show changes

The Twelf Project:TwelfTag

2010-09-01T13:59:48Z

The tag for syntax highlighting:

← Older revision		Revision as of 13:59, 1 September 2010
(One intermediate revision not shown)
Line 7:		Line 7:
	However, the <tt><nowiki><twelf></nowiki></tt> tag is the only way to access the powerful features described below, utilizes a superior syntax highlighter written in Haskell, and does various other nice things. For instance, it crops out any whitespace at the beginning or end of the environment so that this:		However, the <tt><nowiki><twelf></nowiki></tt> tag is the only way to access the powerful features described below, utilizes a superior syntax highlighter written in Haskell, and does various other nice things. For instance, it crops out any whitespace at the beginning or end of the environment so that this:

-	<~~code~~><twelf>	+	<pre><twelf>

	exp : type.		exp : type.
Line 13:		Line 13:
	abs : (exp -> exp) -> exp.		abs : (exp -> exp) -> exp.

-	</twelf></~~code~~>	+	</twelf></pre>

	Will look like this:		Will look like this:

The Twelf Project:TwelfTag

2010-09-01T09:05:18Z

Killing Quick Check for the moment, sadly.

← Older revision		Revision as of 09:05, 1 September 2010
Line 186:		Line 186:

	<twelflink include="natsimple">See hidden code added</twelflink>		<twelflink include="natsimple">See hidden code added</twelflink>
-
-	~~== Quick check ==~~
-
-	On edit pages, there is a button labeled "Quick Twelf check" that will check your Twelf code without leaving the edit page. It will collect all of the bare <nowiki><twelf>...</twelf></nowiki> code, submit it to the Twelf server, and open a box with Twelf's output right below the button. You may immediately edit the code within the edit window and press the button again to check it again. This currently does not work with the <tt>name</tt>, <tt>check="decl"</tt>, but it may soon.

	== TwelfTag and caching ==		== TwelfTag and caching ==

File:POPL Tutorial-scslogo.gif

2010-09-01T07:50:44Z

uploaded a new version of "[[File:POPL Tutorial-scslogo.gif]]"

Lax logic

2010-09-01T06:20:42Z

← Older revision		Revision as of 06:20, 1 September 2010
Line 1:		Line 1:
	%{ In this article, we will take a presentation of a logic very close to		%{ In this article, we will take a presentation of a logic very close to
-	that of Fairtlough and Mendler's lax logic<ref>{{bibtex:fm97lax}}</ref> and	+	that of Fairtlough and Mendler's lax logic<ref >{{bibtex:fm97lax}}</ref> and
	show a translation into a polarized version of Pfenning and Davies' judgmental		show a translation into a polarized version of Pfenning and Davies' judgmental
	reconstruction of lax logic.<ref>{{bibtex:pd01modal}}</ref> We will refer to		reconstruction of lax logic.<ref>{{bibtex:pd01modal}}</ref> We will refer to

MediaWiki:Copyrightwarning

2010-09-01T06:05:28Z

Turning off AJALF for now; it was in any case never made compatible with Literate Twelf, which is the more common style.