index_33.html

Parameters of Coquand's plays.

This is the list of parameters of the game.

In[243]:=

Logic ... ; (* "None", "TarskiPlay", "View" *) ;

In[247]:=

Looking for an assignment in a string.

Assume the string x includes an assignment "... y=n, ... ", or "... y=n". The assignment map computes n.
This is how do it. We remove first all characters until y, then all characters until "=", and in the case there is some "," in the rest of the string, all characters from ","" . What is left is now "n". We compute n out of "n".

In[248]:=

Assignment[x_, y_] := CompoundExpression[val = EraseUntil[x, y] ; val = EraseU ... ringMemberQ[val, ","], val = EraseFrom[val, ","]] ; ToExpression[val]]

An example.

In[249]:=

Out[249]=

In[250]:=

Out[250]=

Out[251]=

In[252]:=

Out[252]=

In[253]:=

Out[253]=

In[254]:=

Out[254]=

In[255]:=

Out[255]=

In[256]:=

Out[256]=

Clearing symbols.

This map takes a string "s", including one symbol, and clears the symbol s.

In[257]:=

This map takes a string "s1, ..., sn", including a list of symbols, and no blanks, and clears all symbols s1, ..., sn.

In[258]:=

ClearList0[S_String] := If[StringMemberQ[S, ","], CompoundEx ... [S, ","]], ClearList0[EraseUntil[S, ","]]], ClearString[S] ; ]

This map removes all blanks first.

In[259]:=

An example.

In[260]:=

Out[260]=

We clear all symbols but a5.

In[261]:=

In[262]:=

Out[262]=

Assigning symbols.

This map takes the left-hand-side "f(x1,...,xn)" of a definition "f(x1,...,xn) = ...", and turns it into the left-hand-side "f[x1_,...,xn_]" of a Mathematica assignment. We replace round by square brackets, and we add an underscore after each variable.

In[263]:=

$LeftHandSide[X_] := StringReplace[X, {"(" ... 2371;","  "_,"}]$

This map takes a term "t", with constants, variables and function symbols, in round brackets notation, and turns it into square brackets notation.

In[264]:=

$Term[E_] := StringReplace[E, {"("  ... 62371;")"  "]"}]$

This map takes two strings "f(x1,...,xn)" and "P(x1,...,xn)" (with P polynomial), and combines them into a Mathematica assignment "f[x1_,...,xn_]:=P(x1,...,xn)".

In[265]:=

This map takes two strings "f(x1,...,xn)" and "t" (with t term in round brackets notation), and combines them into a Mathematica assignment "f[x1_,...,xn_]:=t" .

In[266]:=

This map takes one strings "f(x1,...,xn) =P(x1,...,xn)", and turns it into a Mathematica assignment f[x1_,...,xn_]:=P(x1,...,xn).

In[267]:=

This map takes one strings "f(x1,...,xn) =t" (with t term in round brackets notation), and turns it into a Mathematica assignment "f[x1_,...,xn_]:=t".

In[268]:=

An example.

In[269]:=

In[270]:=

In[272]:=

Out[272]=

Out[273]=

In[274]:=

Global`f

Global`g

g[x_, y_] := h[x, k[y]]

In[276]:=

Computing Game Parameters

This map asks for a string x, then update game parameters according to the content of the string x.

In[277]:=

This map updates logic parameters according to the content of the string x.

In[278]:=

LogicParameters[x_] := CompoundExpression[(* Cut - Free or CutRule ? *) ... f[StringMemberQ[x, "Constructive*Implication"], MaterialImplication = False] ;] 

This map updates graphic parameters according to the content of the string x.

In[279]:=

GraphicParameters[x_] := CompoundExpression[(* FontSize : the integer value *) ... ringMemberQ[x, "Height*="], LevelHeight = Assignment[x, "Height"]] ; ]

This map updates language parameters according to the content of the string x.

In[280]:=

LanguageParameters[x_] := CompoundExpression[(* Symbol : the symbol list of th ... emberQ[x, "Term"], TermAssignment[ EraseUntil[x, "Term"]]] ; ]

This map updates all parameters according to the content of the string x.

In[281]:=

An example.

In[282]:=

We check that game parameters have been assigned correctly.

In[283]:=

Out[283]=

Created by Mathematica (October 17, 2006)