Proof: Difference between revisions
→{{header|Phix}}
Line 725:
even_plus (ES em) en = ES (even_plus em en)
</lang>
=={{header|Phix}}==
Silly text-based version, just for fun.<br>
Obviously 1.1/1.2/1.3 are (loosely) eumlated by the strings "int"/"even"/"odd", and addition by axioms[4].<br>
Clearly 3.2 and 3.3 are not attempted, and I'm not sure which of 3.4/4.1/4.2 the last test is
closest to, or for that matter what the difference between them is supposed to be.
<lang Phix>constant axioms = {{"even+1","odd"},
{"even","2*int"},
{"2*int+2*int","2*(int+int)"},
{"(int+int)","int"},
{"2*int","even"},
{"odd","2*int+1"}}
procedure proof(string a, b)
-- try to convert a into b using only the above axioms
string w = a
sequence seen = {} -- (avoid infinite loops)
while not find(w,seen) do
seen = append(seen,w)
?w
if w=b then exit end if
integer hit = 0
for i=1 to length(axioms) do
string {r,s} = axioms[i]
integer k = match(r,w)
if k then
w[k..k+length(r)-1] = s
hit = i
exit
end if
end for
if hit=0 then exit end if
puts(1,"== ")
end while
?{a,b,iff(w=b?"true","false")}
end procedure
proof("even+even","even")
proof("even+1","odd")
--bad proofs:
proof("int","even")
proof("even+even","odd")</lang>
{{out}}
<pre>
"even+even"
== "2*int+even"
== "2*int+2*int"
== "2*(int+int)"
== "2*int"
== "even"
{"even+even","even","true"}
"even+1"
== "odd"
{"even+1","odd","true"}
"int"
{"int","even","false"}
"even+even"
== "2*int+even"
== "2*int+2*int"
== "2*(int+int)"
== "2*int"
== "even"
== {"even+even","odd","false"}
</pre>
=={{header|Salmon}}==
| |||