Proof: Difference between revisions

Content added Content deleted
m (→‎{{header|Phix}}: syntax coloured)
Line 1,213: Line 1,213:
Clearly 3.2 and 3.3 are not attempted, and I'm not sure which of 3.4/4.1/4.2 the last axiom is
Clearly 3.2 and 3.3 are not attempted, and I'm not sure which of 3.4/4.1/4.2 the last axiom is
closest to, or for that matter what the difference between them is supposed to be.
closest to, or for that matter what the difference between them is supposed to be.
<lang Phix>constant axioms = {{"even+1","odd"},
<!--<lang Phix>(phixonline)-->
<span style="color: #008080;">with</span> <span style="color: #008080;">javascript_semantics</span>
{"even","2*int"},
<span style="color: #008080;">constant</span> <span style="color: #000000;">axioms</span> <span style="color: #0000FF;">=</span> <span style="color: #0000FF;">{{</span><span style="color: #008000;">"even+1"</span><span style="color: #0000FF;">,</span><span style="color: #008000;">"odd"</span><span style="color: #0000FF;">},</span>
{"2*int+2*int","2*(int+int)"},
<span style="color: #0000FF;">{</span><span style="color: #008000;">"even"</span><span style="color: #0000FF;">,</span><span style="color: #008000;">"2*int"</span><span style="color: #0000FF;">},</span>
{"(int+int)","int"},
<span style="color: #0000FF;">{</span><span style="color: #008000;">"2*int+2*int"</span><span style="color: #0000FF;">,</span><span style="color: #008000;">"2*(int+int)"</span><span style="color: #0000FF;">},</span>
{"2*int","even"},
<span style="color: #0000FF;">{</span><span style="color: #008000;">"(int+int)"</span><span style="color: #0000FF;">,</span><span style="color: #008000;">"int"</span><span style="color: #0000FF;">},</span>
{"odd","2*int+1"}}
<span style="color: #0000FF;">{</span><span style="color: #008000;">"2*int"</span><span style="color: #0000FF;">,</span><span style="color: #008000;">"even"</span><span style="color: #0000FF;">},</span>
<span style="color: #0000FF;">{</span><span style="color: #008000;">"odd"</span><span style="color: #0000FF;">,</span><span style="color: #008000;">"2*int+1"</span><span style="color: #0000FF;">}}</span>
procedure proof(string a, b)
⚫
-- try to convert a into b using only the above axioms
<span style="color: #008080;">procedure</span> <span style="color: #000000;">proof</span><span style="color: #0000FF;">(</span><span style="color: #004080;">string</span> <span style="color: #000000;">a</span><span style="color: #0000FF;">,</span> <span style="color: #000000;">b</span><span style="color: #0000FF;">)</span>
string w = a
⚫
<span style="color: #000080;font-style:italic;">-- try to convert a into b using only the above axioms</span>
sequence seen = {} -- (avoid infinite loops)
<span style="color: #004080;">string</span> <span style="color: #000000;">w</span> <span style="color: #0000FF;">=</span> <span style="color: #000000;">a</span>
while not find(w,seen) do
<span style="color: #004080;">sequence</span> <span style="color: #000000;">seen</span> <span style="color: #0000FF;">=</span> <span style="color: #0000FF;">{}</span> <span style="color: #000080;font-style:italic;">-- (avoid infinite loops)</span>
seen = append(seen,w)
<span style="color: #008080;">while</span> <span style="color: #008080;">not</span> <span style="color: #7060A8;">find</span><span style="color: #0000FF;">(</span><span style="color: #000000;">w</span><span style="color: #0000FF;">,</span><span style="color: #000000;">seen</span><span style="color: #0000FF;">)</span> <span style="color: #008080;">do</span>
?w
<span style="color: #000000;">seen</span> <span style="color: #0000FF;">=</span> <span style="color: #7060A8;">append</span><span style="color: #0000FF;">(</span><span style="color: #000000;">seen</span><span style="color: #0000FF;">,</span><span style="color: #000000;">w</span><span style="color: #0000FF;">)</span>
if w=b then exit end if
<span style="color: #0000FF;">?</span><span style="color: #000000;">w</span>
integer hit = 0
<span style="color: #008080;">if</span> <span style="color: #000000;">w</span><span style="color: #0000FF;">=</span><span style="color: #000000;">b</span> <span style="color: #008080;">then</span> <span style="color: #008080;">exit</span> <span style="color: #008080;">end</span> <span style="color: #008080;">if</span>
for i=1 to length(axioms) do
<span style="color: #004080;">integer</span> <span style="color: #000000;">hit</span> <span style="color: #0000FF;">=</span> <span style="color: #000000;">0</span>
string {r,s} = axioms[i]
<span style="color: #008080;">for</span> <span style="color: #000000;">i</span><span style="color: #0000FF;">=</span><span style="color: #000000;">1</span> <span style="color: #008080;">to</span> <span style="color: #7060A8;">length</span><span style="color: #0000FF;">(</span><span style="color: #000000;">axioms</span><span style="color: #0000FF;">)</span> <span style="color: #008080;">do</span>
integer k = match(r,w)
<span style="color: #004080;">string</span> <span style="color: #0000FF;">{</span><span style="color: #000000;">r</span><span style="color: #0000FF;">,</span><span style="color: #000000;">s</span><span style="color: #0000FF;">}</span> <span style="color: #0000FF;">=</span> <span style="color: #000000;">axioms</span><span style="color: #0000FF;">[</span><span style="color: #000000;">i</span><span style="color: #0000FF;">]</span>
if k then
<span style="color: #004080;">integer</span> <span style="color: #000000;">k</span> <span style="color: #0000FF;">=</span> <span style="color: #7060A8;">match</span><span style="color: #0000FF;">(</span><span style="color: #000000;">r</span><span style="color: #0000FF;">,</span><span style="color: #000000;">w</span><span style="color: #0000FF;">)</span>
w[k..k+length(r)-1] = s
<span style="color: #008080;">if</span> <span style="color: #000000;">k</span> <span style="color: #008080;">then</span>
hit = i
<span style="color: #000000;">w</span><span style="color: #0000FF;">[</span><span style="color: #000000;">k</span><span style="color: #0000FF;">..</span><span style="color: #000000;">k</span><span style="color: #0000FF;">+</span><span style="color: #7060A8;">length</span><span style="color: #0000FF;">(</span><span style="color: #000000;">r</span><span style="color: #0000FF;">)-</span><span style="color: #000000;">1</span><span style="color: #0000FF;">]</span> <span style="color: #0000FF;">=</span> <span style="color: #000000;">s</span>
exit
<span style="color: #000000;">hit</span> <span style="color: #0000FF;">=</span> <span style="color: #000000;">i</span>
end if
<span style="color: #008080;">exit</span>
end for
<span style="color: #008080;">end</span> <span style="color: #008080;">if</span>
if hit=0 then exit end if
<span style="color: #008080;">end</span> <span style="color: #008080;">for</span>
puts(1,"== ")
<span style="color: #008080;">if</span> <span style="color: #000000;">hit</span><span style="color: #0000FF;">=</span><span style="color: #000000;">0</span> <span style="color: #008080;">then</span> <span style="color: #008080;">exit</span> <span style="color: #008080;">end</span> <span style="color: #008080;">if</span>
end while
<span style="color: #7060A8;">puts</span><span style="color: #0000FF;">(</span><span style="color: #000000;">1</span><span style="color: #0000FF;">,</span><span style="color: #008000;">"== "</span><span style="color: #0000FF;">)</span>
?{a,b,iff(w=b?"true","false")}
<span style="color: #008080;">end</span> <span style="color: #008080;">while</span>
end procedure
<span style="color: #0000FF;">?{</span><span style="color: #000000;">a</span><span style="color: #0000FF;">,</span><span style="color: #000000;">b</span><span style="color: #0000FF;">,</span><span style="color: #008080;">iff</span><span style="color: #0000FF;">(</span><span style="color: #000000;">w</span><span style="color: #0000FF;">=</span><span style="color: #000000;">b</span><span style="color: #0000FF;">?</span><span style="color: #008000;">"true"</span><span style="color: #0000FF;">,</span><span style="color: #008000;">"false"</span><span style="color: #0000FF;">)}</span>

<span style="color: #008080;">end</span> <span style="color: #008080;">procedure</span>
proof("even+even","even")
proof("even+1","odd")
<span style="color: #000000;">proof</span><span style="color: #0000FF;">(</span><span style="color: #008000;">"even+even"</span><span style="color: #0000FF;">,</span><span style="color: #008000;">"even"</span><span style="color: #0000FF;">)</span>
--bad proofs:
<span style="color: #000000;">proof</span><span style="color: #0000FF;">(</span><span style="color: #008000;">"even+1"</span><span style="color: #0000FF;">,</span><span style="color: #008000;">"odd"</span><span style="color: #0000FF;">)</span>
proof("int","even")
<span style="color: #000080;font-style:italic;">--bad proofs:</span>
proof("even+even","odd")</lang>
<span style="color: #000000;">proof</span><span style="color: #0000FF;">(</span><span style="color: #008000;">"int"</span><span style="color: #0000FF;">,</span><span style="color: #008000;">"even"</span><span style="color: #0000FF;">)</span>
<span style="color: #000000;">proof</span><span style="color: #0000FF;">(</span><span style="color: #008000;">"even+even"</span><span style="color: #0000FF;">,</span><span style="color: #008000;">"odd"</span><span style="color: #0000FF;">)</span>
<!--</lang>-->
{{out}}
{{out}}
<pre>
<pre>
Retrieved from "https://rosettacode.org/wiki/Proof"