// JavaScript Program to implement an equational decision procedure for lattice-ordered groups // version of 11 Feb 2003, by Peter Jipsen, http://www.chapman.edu/jipsen // The code has three main parts to it: // 1. Handling formulas (actually only the part about equations and inequations is used) // parsing the ascii input and writing html output. // 2. Implementing the decision procedure. // 3. Administering the l-group quiz // Part 1. Handling formulas //check if the symbol font is available symb = navigator.appVersion.lastIndexOf('Win')!=-1 || navigator.appVersion.lastIndexOf('Mac')!=-1; function out(col,str,alt,sp) { return sp+""+str : (symb?" >"+str : ">"+alt))+""+sp; } bl=" "; avar = {name:"a", arity:0, output:"a"}; bvar = {name:"b", arity:0, output:"b"}; cvar = {name:"c", arity:0, output:"c"}; dvar = {name:"d", arity:0, output:"d"}; Avar = {name:"A", arity:0, output:"A"}; Bvar = {name:"B", arity:0, output:"B"}; Cvar = {name:"C", arity:0, output:"C"}; Dvar = {name:"D", arity:0, output:"D"}; xvar = {name:"x", arity:0, output:"x"}; yvar = {name:"y", arity:0, output:"y"}; zvar = {name:"z", arity:0, output:"z"}; Xvar = {name:"X", arity:0, output:"X"}; Yvar = {name:"Y", arity:0, output:"Y"}; Zvar = {name:"Z", arity:0, output:"Z"}; vari = [ avar, Avar, bvar, Bvar, cvar, Cvar, dvar, Dvar, xvar, Xvar, yvar, Yvar, zvar, Zvar ]; unit = {name:"e", arity:0, output:"e"}; cons = [unit]; meet = {name:"^", arity:2, priority:6, output:out("Blue","∧","^",bl), infix:true, paren:true}; join = {name:"v", arity:2, priority:6, output:out("Blue","∨","v",bl), infix:true, paren:true}; times = {name:"*", arity:2, priority:8, output:out("Blue","*","*",""), infix:true, paren:true}; over = {name:"/", arity:2, priority:8, output:'/', infix:true, paren:true}; under = {name:"\\", arity:2, priority:8, output:'\\', infix:true, paren:true}; oper = [ meet, join, times, over, under ]; eq = {name:"=", arity:2, output:' = ', infix:true, priority:4}; leq = {name:"<=", arity:2, output:out("Red","≤","<=",bl), infix:true, priority:4}; geq = {name:">=", arity:2, output:out("Red","≥",">=",bl), infix:true, priority:4}; pred = [ eq, leq, geq ]; for (var i=0; i~'}; impSymbol = {name:"->", arity:2, priority:1, output:' ==> ', infix:true,paren:true}; andSymbol = {name:"and", arity:2, priority:3, output:'  and  ', infix:true,paren:true}; orSymbol = {name:"or", arity:2, priority:2, output:'  or  ', infix:true,paren:true}; iffSymbol = {name:"iff", arity:2, priority:0, output:'   iff   ', infix:true,paren:true}; allSymbol = {name:"A", arity:2, output:'"'}; exSymbol = {name:"E", arity:2, output:'\$'}; conn = [notSymbol, andSymbol, orSymbol, impSymbol, iffSymbol, allSymbol, exSymbol]; comma = {name:",", punc:true}; leftBracket = {name:"(", punc:true}; rightBracket = {name:")", punc:true}; leftSqBracket = {name:"[", punc:true}; rightSqBracket = {name:"]", punc:true}; punc = [comma, leftSqBracket, rightSqBracket, leftBracket, rightBracket ]; function add(arr, elt){ // the push method is not supported in IExpl*der arr[arr.length]=elt; } function Expr(symbol, arg, priority){ // third argument only used during parsing this.symbol = symbol; this.arg = arg; this.priority = priority; } function randomInt(n) { return Math.floor(n*Math.random()); } function randomElt(a) { return a[Math.floor(a.length*Math.random())]; } function randomVari(){ return new Expr(randomElt(vari.slice(8)), []) } function randomList(len,max){ //random list of values in [0..max-1] with one of them = max-1 var l=[]; for (var i=0; i 0) { var op=randomElt(oper); var dep=randomList(op.arity,depth); var arg=[]; for (var i=0; i 0) { var co=randomElt(conn); if (co==allSymbol || co==exSymbol){ var arg = [randomVari(), randomFormula(fDepth-1,tDepth)]; return new Expr(co, arg); } var dep=randomList(co.arity,fDepth); var arg=[]; for (var i=0; i s2.name) return 1 else return -1; } symbols = vari.concat(cons, oper, pred, conn, punc); symbols.sort(compareNames); names = []; for (var i=0; imaxPriority) maxPriority = symbols[i].priority; maxPriority++; //names should contain no blanks function removeCharsAndBlanks(str,n) { var st = str.slice(n); for (var i=0; i=str } function getSymbol(str) { var k=0; var j=0; var st=""; var oldst=""; var more = true; for (var i=1; i<=str.length && more; i++) { oldst=st; st=str.slice(0,i); j=k; k=position(names, st, j); more = (ksymbol.priority || (right.priority==symbol.priority && right.symbol.rightparen)) { expr=new Expr(symbol, [expr,right], symbol.priority); } else { insert=right; while (insert.arg[0].priority && insert.arg[0].prioritysymbol.priority || insert.arg[0].symbol.rightparen) { expr=new Expr(symbol, [expr,insert.arg[0]], symbol.priority); insert.arg[0]=expr; } else { expr=new Expr(symbol, [expr,insert.arg[0].arg[0]], symbol.priority); insert.arg[0].arg[0]=expr; } expr=right; } return [expr,str]; } function parse(str) { var temp = str2expr(str); if (temp[1].slice(0,5)=="Error") document.write("

"+temp[1]+"

"); else if (temp[1].slice(0,5)!="") document.write("

Parse Leftover: "+temp[1]+"

"); //still have to check arities of expressions return temp[0]; } function outputList(li) { for (var i=0; i=str } function inverse(v) { if (v=="x") return "X"; if (v=="X") return "x"; if (v=="y") return "Y"; if (v=="Y") return "y"; if (v=="z") return "Z"; if (v=="Z") return "z"; if (v=="a") return "A"; if (v=="A") return "a"; if (v=="b") return "B"; if (v=="B") return "b"; if (v=="c") return "C"; if (v=="C") return "c"; if (v=="d") return "D"; if (v=="D") return "d"; return "Error"; } function invert(t) { if (t.symbol==unit) return t; if (t.symbol.name=="A") return new Expr(vari[0], []); if (t.symbol.name=="a") return new Expr(vari[1], []); if (t.symbol.name=="B") return new Expr(vari[2], []); if (t.symbol.name=="b") return new Expr(vari[3], []); if (t.symbol.name=="C") return new Expr(vari[4], []); if (t.symbol.name=="c") return new Expr(vari[5], []); if (t.symbol.name=="D") return new Expr(vari[6], []); if (t.symbol.name=="d") return new Expr(vari[7], []); if (t.symbol.name=="X") return new Expr(vari[8], []); if (t.symbol.name=="x") return new Expr(vari[9], []); if (t.symbol.name=="Y") return new Expr(vari[10], []); if (t.symbol.name=="y") return new Expr(vari[11], []); if (t.symbol.name=="Z") return new Expr(vari[12], []); if (t.symbol.name=="z") return new Expr(vari[13], []); if (t.symbol==meet) return new Expr(join,[invert(t.arg[0]),invert(t.arg[1])]); if (t.symbol==join) return new Expr(meet,[invert(t.arg[0]),invert(t.arg[1])]); if (t.symbol==times) return new Expr(times,[invert(t.arg[1]),invert(t.arg[0])]); if (t.symbol==over) return new Expr(times,[t.arg[1],invert(t.arg[0])]); if (t.symbol==under) return new Expr(times,[invert(t.arg[1]),t.arg[0]]); } function trou(t) { if (t.symbol==unit || t.symbol.vari) return t; if (t.symbol==meet || t.symbol==join || t.symbol==times) return new Expr(t.symbol,[trou(t.arg[0]),trou(t.arg[1])]); if (t.symbol==over) return new Expr(times,[trou(t.arg[0]),invert(trou(t.arg[1]))]); if (t.symbol==under) return new Expr(times,[invert(trou(t.arg[0])),trou(t.arg[1])]); alert("error "+t.symbol); } function negcone(t) { if (t.symbol==unit) return t; if (t.symbol.vari) return new Expr(meet, [t,new Expr(unit,[])]); if (t.symbol==over) return new Expr(meet, [new Expr(over,[negcone(t.arg[0]),negcone(t.arg[1])]),new Expr(unit,[])]); if (t.symbol==under) return new Expr(meet, [new Expr(under,[negcone(t.arg[0]),negcone(t.arg[1])]),new Expr(unit,[])]); if (t.symbol==times) return new Expr(times,[negcone(t.arg[0]),negcone(t.arg[1])]); if (t.symbol==join) return new Expr(join,[negcone(t.arg[0]),negcone(t.arg[1])]); if (t.symbol==meet) return new Expr(meet,[negcone(t.arg[0]),negcone(t.arg[1])]); } function gmv(t) { if (t.symbol==unit) return t; if (t.symbol.vari) return new Expr(join, [t,new Expr(vari[6],[])]); if (t.symbol==over) return new Expr(over,[gmv(t.arg[0]),gmv(t.arg[1])]); if (t.symbol==under) return new Expr(under,[gmv(t.arg[0]),gmv(t.arg[1])]); if (t.symbol==times) return new Expr(join, [new Expr(times,[gmv(t.arg[0]),gmv(t.arg[1])]),new Expr(vari[6],[])]); if (t.symbol==join) return new Expr(join,[gmv(t.arg[0]),gmv(t.arg[1])]); if (t.symbol==meet) return new Expr(meet,[gmv(t.arg[0]),gmv(t.arg[1])]); } function objToString(a) { var st=""; //document.write("\n
type=",typeof a); if (typeof a =="string") st="\""+a+"\""; else if (a.length>0) { for (var i=0; iAssignmentsList w="+w+" v="+v+" a.length="+a.length); for (j=i+1; jevaluateLGterm t.symbol.name="+t.symbol.name); if (t.symbol.vari) { var n=a[i].length; var w; if (n>0 && t.symbol.name==inverse(a[i].charAt(n-1))) w=a[i].slice(0,n-1); else w=a[i]+t.symbol.name; j=position1(a,w); if (j!=a.length) return [[a,j]]; else return assignmentsList(a,i,w,t.symbol.name); } if (t.symbol==times) { al=evaluateLGterm(t.arg[0],a,i); bl=[]; for (var k=0; k=bl[n][1]) add(cl,bl[n]); else add(cl,[bl[n][0],j1]); } } return cl; } } function isTermPositive(t) { var al=evaluateLGterm(t,[""],0); //document.write("\n
Number of diagrams checked = ",al.length); // " al=",objToString(al)); for (var i=0; ial[i][1]) { //document.write(", fails at ",objToString(al[i])); return [false,al,i,t]; } return [true,al,0,t]; } function isTermIdentity(t) { var al=evaluateLGterm(t,[""],0); //document.write("\n
Number of diagrams checked = ",al.length); for (var i=0; iCorrect, "+st+", 1 point."); return score+1; } function wrong(win, score, st) { win.document.write("Wrong, "+st+", -1 point."); return score-1; } function comment(win, st) { win.document.write("

"+st+"
"); } function check(frm) { //analyse the radio buttons and output results win=open("", "resultWindow", "height=450,width=750,menubar=yes,resizable=yes,scrollbars=yes"); win.document.open(); var score=0; win.document.write("Quiz Results"); win.document.write("

### "+ "Results for your personalised Quiz 1

"); for (var i=0; i"); } win.document.write("

### "+ "Your Score is "+score+"/"+inequations.length+"

"); if (score<1) comment(win,"Guessing will get you nowhere :-)"); else if (score
Click the X in the top right '+ 'hand corner to close this window
'); win.document.write('

Here are the lgroup diagrams '+ 'for the above inequalities:'); for (var i=0; i"+(i+1)+".   "+e2s(inequations[i])+"

"+ objToString(checkEquation(inequations[i])[1])); } win.document.write(""); win.document.close(); }