verify_typed_views.py

#!/usr/bin/env python3
"""Finite typed-template and mixed-history controls, not a universal proof."""
import json
from itertools import product

# One branch: X=aT, Y=U, P=aTU, exposed T:L.
old=frozenset({('','L'),('a','L'),('b','L'),('aT','L'),('U','L'),('aTU','R'),('T','L')})
states={old}; found=None;counts=[]
for k in range(2):
    ok=any({('T','L'),('U','L'),('TU','R')} <= s for s in states)
    if ok and found is None:found=k
    counts.append(len(states))
    if k==0:
        nxt=set()
        for s in states:
            for w,t in s:
                if t=='L':
                    for c in 'ab':nxt.add(s|{(c+w,'L')})
                for v,_ in s:nxt.add(s|{(w+v,'R')})
        states=nxt
assert found==1
assert ('aTU','L') not in old # Returning cached P as a list is illegal.
assert 'aTU'+'U'=='aTUU' # The ill-sorted join still satisfies its word equation.

class Arena:
    def __init__(self):
        self.nodes=[('E',)];self.words=[''];self.types=['L']
    def cons(self,c,x):
        assert self.types[x]=='L'
        self.nodes.append(('Cons',c,x));self.words.append(c+self.words[x]);self.types.append('L')
        return len(self.nodes)-1
    def cat(self,x,y):
        self.nodes.append(('Cat',x,y));self.words.append(self.words[x]+self.words[y]);self.types.append('R')
        return len(self.nodes)-1

def step(ar,x,p,i,letter):
    old=len(ar.nodes);xx=list(x);pp=list(p)
    if letter is None:
        if ar.nodes[x[i]][0]=='E':return x,p,0,'empty'
        _,head,tail=ar.nodes[x[i]];xx[i]=tail
    else:head='pushed';xx[i]=ar.cons(letter,x[i])
    if i==0:pp[0]=xx[0]
    else:pp[i]=ar.cat(pp[i-1],xx[i])
    for j in range(i+1,len(x)):pp[j]=ar.cat(pp[j-1],x[j])
    return tuple(xx),tuple(pp),len(ar.nodes)-old,head

def valid(ar,x,p):
    w=''
    for j in range(len(x)):
        assert ar.types[x[j]]=='L';w+=ar.words[x[j]];assert ar.words[p[j]]==w

rows=[]
for d in range(1,4):
    ar=Arena();calls=0
    def walk(x,p,depth):
        global calls
        valid(ar,x,p)
        if depth==0:return
        old=tuple(ar.nodes); vals=tuple(ar.words[v] for v in x+p)
        for i,c in product(range(d),('a','b',None)):
            before=ar.words[x[i]]
            xx,pp,cost,head=step(ar,x,p,i,c)
            assert tuple(ar.nodes[:len(old)])==old
            assert tuple(ar.words[v] for v in x+p)==vals
            expected=(c+before) if c else before[1:]
            assert ar.words[xx[i]]==expected
            if c:assert cost==(d if i==0 else d-i+1)
            elif before:
                assert head==before[0];assert cost==(d-1 if i==0 else d-i)
            else:assert cost==0 and head=='empty'
            calls+=1;walk(xx,pp,depth-1)
    walk((0,)*d,(0,)*d,4)
    rows.append({'d':d,'mixed_calls_through_depth_four':calls})

# Concrete lower-bound family: old proper lists ending in b have length <=1.
for n in range(1,13):
    ar=Arena();aa=ar.cons('a',0);bb=ar.cons('b',0);x=0
    for _ in range(n):x=ar.cons('a',x)
    p=ar.cat(x,bb)
    assert ar.words[p]=='a'*n+'b' and ar.types[p]=='R'
    assert max(len(w) for w,t in zip(ar.words,ar.types) if t=='L' and w.endswith('b'))==1
print(json.dumps({'scope':'One head-a branch typed-template enumeration through K=1; all mixed binary push/pop histories through depth 4 for d=1..3, with old versions retained; proper-list catenation witness n=1..12. No proof-assistant verification or unbounded completeness check.','typed_template_state_counts':counts,'pop_cache_minimum_in_test':found,'history_checks':rows},indent=2))