|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
-- zha.lua: the ZHA class for dednat5.
-- This file:
-- http://angg.twu.net/dednat5/zha.lua
-- http://angg.twu.net/dednat5/zha.lua.html
-- (find-angg "dednat5/zha.lua")
--
-- From: (find-angg "sheavesforchildren/zhas.lua")
--
-- This implements a class for calculating with ZHAs.
-- Includes drawing tools, quick ways to compute and/or/imp/not/etc,
-- and a quick way to apply modalities.
-- «.ZHA» (to "ZHA")
-- «.ZHA-tests» (to "ZHA-tests")
-- «.ZHA-tests-bf» (to "ZHA-tests-bf")
-- «.ZHA-tests-fourman» (to "ZHA-tests-fourman")
-- «.ZHA-tests-imp» (to "ZHA-tests-imp")
require "wrap" -- (find-dn5file "wrap.lua" "__mul")
-- (find-angg "LUA/lua50init.lua" "eval-and-L")
-- «ZHA» (to ".ZHA")
ZHA = Class {
type = "ZHA",
specN = function (spec)
local copydigit = function (s) return s:sub(1, 1):rep(#s) end
return (spec:gsub("[1-9][LRV]+", copydigit))
end,
fromspec = function (spec)
local z = ZHA {spec = spec}
z.specN = ZHA.specN(spec)
z.maxy = #spec - 1
local relL, relR = 0, 0
local minx, maxx = 0, 0
for y=1,z.maxy do
local a, deltaL, deltaR = z:yaction(y)
relL = relL + deltaL
relR = relR + deltaR
minx = min(relL, minx)
maxx = max(relR, maxx)
end
z.x0 = - minx
z.L = {[0] = z.x0}
z.R = {[0] = z.x0}
z.maxx = - minx + maxx
for y=1,z.maxy do
local a, deltaL, deltaR = z:yaction(y)
z.L[y] = z.L[y-1] + deltaL
z.R[y] = z.R[y-1] + deltaR
end
return z
end,
fromspeclr = function (spec)
return ZHA.fromspec(spec):calclrminmax()
end,
--
__index = {
yC = function (z, y) return z.spec :sub(y+1, y+1) end,
yN = function (z, y) return tonumber(z.specN:sub(y+1, y+1)) end,
yaction = function (z, y)
if z:yC(y) == "L" then return "L", -1, -1 end
if z:yC(y) == "R" then return "R", 1, 1 end
if z:yC(y) == "V" then return "V", 0, 0 end
if z:yN(y) == z:yN(y-1)+1 then return "+", -1, 1 end
if z:yN(y) == z:yN(y-1)-1 then return "-", 1, -1 end
end,
--
-- Coordinates, both (x,y) and (l,r)
xytol = function (z, x, y) return (y - (x - z.x0)) / 2 end,
xytor = function (z, x, y) return (y + (x - z.x0)) / 2 end,
xytolr0 = function (z, x, y) return z:xytol(x, y), z:xytor(x, y) end,
xytolr = function (z, x, y) return z:xytol(x, y)..z:xytor(x, y) end,
lrtoxy0 = function (z, l, r) return r - l + z.x0, l + r end,
lrtolr0 = function (z, lr)
return tonumber(lr:sub(1, 1)), tonumber(lr:sub(2, 2))
end,
lrtoxy = function (lr)
local l, r = tonumber(lr:sub(1, 1)), tonumber(lr:sub(2, 2))
return lrtoxy0(l, r)
end,
--
-- Compute minl[], maxl[], minr[], maxr[], lrtop
calclrminmax = function (z)
z.minl, z.minr, z.maxl, z.maxr = {}, {}, {}, {}
local minmax = function (a, b, c)
return min((a or b), b), max(b, (c or b))
end
local lrminmax = function (l, r)
z.minl[r], z.maxl[r] = minmax(z.minl[r], l, z.maxl[r])
z.minr[l], z.maxr[l] = minmax(z.minr[l], r, z.maxr[l])
end
for y=0,z.maxy do
lrminmax(z:xytolr0(z.L[y], y))
lrminmax(z:xytolr0(z.R[y], y))
end
z.lrtop = z:xytolr(z.L[z.maxy], z.maxy)
return z
end,
--
-- Drawing (in ascii)
lrline = function (z, y, f)
f = f or function (lr) return lr end
s = string.rep(" ", z.L[y]) .. f(z:xytolr(z.L[y], y))
for x=z.L[y]+2,z.R[y],2 do s = s .. " " .. f(z:xytolr(x, y)) end
return s
end,
odotline = function (z, y)
return string.rep(" ", z.L[y]).."o"..string.rep(".o", z:yN(y) - 1)
end,
drawf = function (z, f)
for y=z.maxy,0,-1 do print(z:lrline(y, f)) end
return z
end,
drawL = function (z, str) z:drawf(L(str)); return z end,
drawE = function (z, str)
local f = L(str)
z:drawf(function (P) return Eq(P, f(P)) end)
return z
end,
--
-- Less or equal (e.g., for testing adjunctions)
le = function (z, Plr, Qlr)
local Pl, Pr = z:lrtolr0(Plr)
local Ql, Qr = z:lrtolr0(Qlr)
return Pl <= Ql and Pr <= Qr
end,
le11 = function (z, Plr, Qlr) return z:le(Plr, Qlr) and "11" or "00" end,
--
-- And, Or, Implies, Not
lrand = function (z, Plr, Qlr)
local Pl, Pr = z:lrtolr0(Plr)
local Ql, Qr = z:lrtolr0(Qlr)
return min(Pl, Ql)..min(Pr, Qr)
end,
lror = function (z, Plr, Qlr)
local Pl, Pr = z:lrtolr0(Plr)
local Ql, Qr = z:lrtolr0(Qlr)
return max(Pl, Ql)..max(Pr, Qr)
end,
lrimp = function (z, Plr, Qlr)
local Pl, Pr = z:lrtolr0(Plr)
local Ql, Qr = z:lrtolr0(Qlr)
if Pl <= Ql and Pr <= Qr then return z.lrtop end
if Pl > Ql and Pr > Qr then return Qlr end
if Pl <= Ql then return z.maxl[Qr]..Qr end
if Ql <= Pl then return Ql..z.maxr[Ql] end
return "??"
end,
lrnot = function (z, Plr) return z:lrimp(Plr, "00") end,
--
-- Modalities
topmostbelowlr0 = function (z, l, r)
if z.maxr[l] <= r then
return l..min(z.maxr[l], r)
else
return min(z.maxl[r], l)..r
end
end,
topmostbelowlr = function (z, lr)
return z:topmostbelowlr0(z:lrtolr0(lr))
end,
modality0 = function (z, lstr, rstr, l, r)
local newl = tonumber(lstr:sub(l+1, l+1))
local newr = tonumber(rstr:sub(r+1, r+1))
return z:topmostbelowlr0(newl, newr)
end,
modality = function (z, lstr, rstr, lr)
return z:modality0(lstr, rstr, z:lrtolr0(lr))
end,
--
-- Drawing the contour and cuts (in LaTeX)
lrtopcoords = function (z, dl, dr, l, r)
-- return format("(%3.1f,%3.1f)", l, r)
-- return format("(%3.1f,%3.1f)", dl+l, dr+r)
local newl,newr = dl+l, dr+r
local x,y = z:lrtoxy0(newl, newr)
return format("(%3.1f,%3.1f)", x, y)
end,
--
outerangles0 = function (z)
local left, right = {}, {}
local l,r = 0,0
while true do
l = z.maxl[r]
table.insert(left, {l=l, r=r}); print("left", l, r)
r = z.minr[l + 1]
if not r then break end
table.insert(left, {l=l, r=r}); print("left", l, r)
end
local l,r = 0,0
while true do
r = z.maxr[l]
table.insert(right, {l=l, r=r}); print("right", l, r)
l = z.minl[r + 1]
if not l then break end
table.insert(right, {l=l, r=r}); print("right", l, r)
end
return left, right
end,
leftcut0 = function (z, l) return z.minr[l+1], z.maxr[l] end,
rightcut0 = function (z, l) return z.minl[r+1], z.maxr[l] end,
--
outerangles = function (z)
local path = {}
local corner = function (dl, dr, l, r)
-- table.insert(path, format("(%f,%f)", l, r))
table.insert(path, z:lrtopcoords(dl, dr, l, r))
end
corner(-0.5, -0.5, 0, 0)
local ltop, rtop = z:lrtolr0(z.lrtop)
local left, right = z:outerangles0()
for _,lr in ipairs(left) do
corner(0.5, -0.5, lr.l, lr.r)
end
corner(0.5, 0.5, ltop, rtop)
for i=#right,1,-1 do
local lr = right[i]
corner(-0.5, 0.5, lr.l, lr.r)
end
corner(-0.5, -0.5, 0, 0)
return " \\draw[outer] "..table.concat(path, " -- ")..";\n"
end,
leftcut = function (z, l)
local r1, r2 = z.minr[l+1], z.maxr[l]
return " \\draw[cut] "..z:lrtopcoords(0.5, -0.5, l, r1).." -- "..
z:lrtopcoords(0.5, 0.5, l, r2)..";\n"
end,
rightcut = function (z, r)
local l1, l2 = z.minl[r+1], z.maxl[r]
return " \\draw[cut] "..z:lrtopcoords(-0.5, 0.5, l1, r).." -- "..
z:lrtopcoords( 0.5, 0.5, l2, r)..";\n"
end,
--
genpoints = function (z)
return cow(function ()
for y=z.maxy,0,-1 do
for x=z.L[y],z.R[y],2 do
local l,r = z:xytolr0(x,y)
coy(z, x, y, l, r)
end
end
end)
end,
},
}
-- zha_utils(): define some global functions
-- for ZHAs, all with very short names
--
zha_utils = function ()
-- Shorthands for some operations
Le = function (P, Q) return z:le11 (P, Q) end
Or = function (P, Q) return z:lror (P, Q) end
And = function (P, Q) return z:lrand(P, Q) end
Imp = function (P, Q) return z:lrimp(P, Q) end
Not = function (P) return z:lrnot(P) end
Top = function () return z.lrtop end
--
Eq = function (P, Q) return P==Q and '11' or '00' end
--
-- Elementary J-operators
-- (find-books "__cats/__cats.el" "fourman")
-- (find-slnm0753page (+ 14 329) "2.18 Elementary J-operators")
Jo = function (P) return
function (Q) return Or(P, Q) end
end
Ji = function (P) return
function (Q) return Imp(P, Q) end
end
Jb = function (R) return
function (Q) return Imp(Imp(Q, R), R) end
end
Jf = function (P, Q) return
function (R) return And(Or(P, R), Imp(Q, R)) end
end
--
Jand = function (J1, J2) return
function (P) return And(J1(P), J2(P)) end
end
Jor = function (J1, J2) return
function (P) return Or(J1(P), J2(P)) end
end
--
-- The generic J-operator:
Jm = function (lstr, rstr) return
function (Q) return z:modality(lstr, rstr, Q) end
end
end
-- M = L "P z:modality('1133556', '02244', P)"
-- M = Jm("1133556", "02244")
--[[
-- «ZHA-tests-bf» (to ".ZHA-tests-bf")
* (eepitch-lua51)
* (eepitch-kill)
* (eepitch-lua51)
dofile "zha.lua"
zha_utils()
-- 2015jun19: Tests for explaining brute force
z = ZHA.fromspeclr("1234567654321"):drawf()
z:drawL "P Not(P) "
q = '42'; r = '24'
z:drawL "P Le(P,q) "
z:drawL "P Le(P,r) "
z:drawL "P And(Le(P,q),Le(P,r)) "
q = '42'; r = '24'
z:drawL "P And(P,q) "
z:drawL "P Le(And(P,q), r) "
z:drawL "P Le(P, Imp(q,r)) "
= Imp(q,r)
-- «ZHA-tests-imp» (to ".ZHA-tests-imp")
* (eepitch-lua51)
* (eepitch-kill)
* (eepitch-lua51)
dofile "zha.lua"
zha_utils()
z = ZHA.fromspeclr("123454321"):drawf()
z:drawL "Q Imp(Q, '22')"
z:drawL "R Imp('22', R)"
-- «ZHA-tests» (to ".ZHA-tests")
-- (find-sfc "zhas.lua" "ZHA-tests")
* (eepitch-lua51)
* (eepitch-kill)
* (eepitch-lua51)
dofile "zha.lua"
zha_utils()
ZHA.fromspeclr("12L1RRR2RL1"):drawf()
ZHA.fromspeclr("123LLR432L1"):drawf()
ZHA.fromspeclr("123RRL432R1"):drawf()
ZHA.fromspeclr("12345RR"):drawf()
ZHA.fromspeclr("12345RRRR4321"):drawf()
z = ZHA.fromspec "123LL432L1"
z = ZHA.fromspeclr("123LL432L1"):drawf()
z:drawL "P Not(P) "
z:drawL "P Not(Not(P)) "
z:drawL "P Eq(P, Not(Not(P)))"
z:drawL "P And(P, '21')"
z:drawL "P Imp(P, '21')"
z:drawL "P Imp('21', P)"
z:drawL "P Le('21', P)"
z:drawL "P Le(P, '21')"
-- Test my definition of "implies":
-- For every Q and R the two "draw"s below
-- should draw the same down-set.
Q, R = "20", "11"
Q, R = "20", "00"
z:drawL "P Le(And(P, Q), R)"
z:drawL "P Le(P, Imp(Q, R))"
-- «ZHA-tests-fourman» (to ".ZHA-tests-fourman")
-- (find-sfc "zhas.lua" "ZHA-tests")
* (eepitch-lua51)
* (eepitch-kill)
* (eepitch-lua51)
dofile "zha.lua"
zha_utils()
-- Elementary J-operators
-- (find-books "__cats/__cats.el" "fourman")
-- (find-slnm0753page (+ 14 329) "2.18 Elementary J-operators")
-- (find-xdvipage "~/LATEX/istanbulquotes.dvi")
Jsub = function (a) return function (p) return Or(a, p) end end
Jsup = function (a) return function (p) return Imp(a, p) end end
Bsub = function (a) return function (p) return Imp(Imp(p, a), a) end end
JJ = function (a, b) return function (p) return And(Or(a, p), Imp(b, p)) end end
z = ZHA.fromspeclr("123454321"):drawf()
z:drawL "p Jsub'22'(p) "
z:drawL "p Jsup'22'(p) "
z:drawL "p Bsub'22'(p) "
z:drawL "p JJ('31','13')(p) "
z = ZHA.fromspeclr("12345678987654321"):drawf()
z:drawL "p JJ('52', '25')(p)"
z:drawL "p Or('52',p) "
z:drawL "p Imp('25',p) "
z:drawL "p And(Or('52',p),Imp('25',p))"
= Imp(Imp('12','23'),'40')
= JJ('12','23')('40')
* (eepitch-lua51)
* (eepitch-kill)
* (eepitch-lua51)
dofile "zha.lua"
zha_utils()
z = ZHA.fromspeclr("1234567654321"):drawf()
My = Jm("0123456", "0123456")
My = Jm("0133456", "0144456")
z:drawf(L "P Eq(P, My(P))")
z:drawL "P Eq(P, My(P))"
z:drawE "P My(P) "
-- (find-books "__cats/__cats.el" "fourman")
-- (find-slnm0753page (+ 14 329) "2.18 Elementary J-operators")
-- (find-slnm0753page (+ 14 329) "(i) J_a p = a v p")
-- (find-slnm0753page (+ 14 330) "(ii) J^a p = a -> p")
z:drawE "P Jo'25' (P)"
z:drawE "P Jo'41' (P)"
z:drawE "P Ji'25' (P)"
z:drawE "P Ji'41' (P)"
-- (find-slnm0753page (+ 14 331) "(i) J_a v J_b = J_avb")
z:drawE "P Jor(Jo'41', Jo'25')(P)"
z:drawE "P Jo(Or('41', '25'))(P)"
-- (find-slnm0753page (+ 14 331) "(ii) J^a v J^b = J_a&b")
z:drawE "P Jor(Ji'41', Ji'25')(P)"
z:drawE "P Ji(And('41', '25'))(P)"
-- (find-slnm0753page (+ 14 331) "(iii) J_a & J_b = J_a&b")
z:drawE "P Jand(Jo'41', Jo'25')(P)"
z:drawE "P Jo(And('41', '25'))(P)"
-- (find-slnm0753page (+ 14 331) "(iv) J^a & J^b = J^avb")
z:drawE "P Jand(Ji'41', Ji'25')(P)"
z:drawE "P Ji(Or('41', '25'))(P)"
-- (find-slnm0753page (+ 14 331) "(v) J_a & J^a = bot")
z:drawE "P Jand(Jo'41', Ji'41')(P)"
-- (find-slnm0753page (+ 14 331) "(vi) J_a v J^a = top")
z:drawE "P Jor(Jo'41', Ji'41')(P)"
-- (find-slnm0753page (+ 14 331) "(vii) J_a v K = K o J_a")
z:drawE "P Jor(Jo'41', My)(P)"
z:drawE "P My(Jo'41'(P))"
-- (find-slnm0753page (+ 14 331) "(viii) J^a v K = J_a o K")
z:drawE "P Jor(Ji'41', My)(P)"
z:drawE "P Ji'41'(My(P))"
-- (find-slnm0753page (+ 14 331) "(ix) J_a v B_a = B_a")
z:drawE "P Jor(Jo'41', Jb'41')(P)"
z:drawE "P Jb'41'(P)"
-- (find-slnm0753page (+ 14 331) "(x) J^a v B_b = B_a->b")
z:drawE "P Jor(Ji'41', Jb'25')(P)"
z:drawE "P Jb(Imp('41', '25'))(P)"
z:drawE "P Jand(Jb'44', Jb'22')(P)"
z:drawE "P Jand(Jand(Jb'44', Jb'22'), Jb'00')(P)"
z:drawE "P Ji(Or('41', '25'))(P)"
z:drawE "P Ji(Or('41', '25'))(P)"
z:drawE "P Jb('23')(P)"
z:drawE "P Jb('41', '25')(P)"
z:drawE "P Jand(Jo'41', Jo'25')(P) "
z:drawE "P Jo(And('41', '25'))(P) "
z:drawf(L "P Eq(P, Jo'41'(P)) ")
z:drawf(L "P Eq(P, Jo'25'(P)) ")
z:drawf(L "P Eq(P, And(Jo'41'(P), Jo'25'(P)))")
z:drawf(L "P Eq(P, Jo(And('41', '25'))(P)) ")
z:drawf(L "P Eq(P, Ji'41'(P)) ")
z:drawf(L "P Eq(P, Ji'25'(P)) ")
z:drawf(L "P Eq(P, And(Ji'41'(P), Ji'25'(P)))")
z:drawf(L "P Eq(P, Jo(And('41', '25'))(P)) ")
-- M = Jm("1133556", "02244")
--]]
-- Local Variables:
-- coding: raw-text-unix
-- End: