Version 11 of forall

Updated 2007-06-21 09:15:59 by dkf

Richard Suchenwirth 2002-05-15 - In return, Lars Hellström used special return codes to handle questions like "for all a in A there exists some b in B such that for all c in C the condition P(a,b,c) holds". It appears as if the same task can be done with nested proc calls (and regular returns), while looking even more similar to the original task specification:

 forall a $A {exists b $B {forall c $C {P $a $b $c}}}

 proc forall {elementName set condition} {
    upvar 1 $elementName element
    foreach element $set {
        if {![uplevel 1 $condition]} {return 0}
    }
    return 1
 }
 proc exists {elementName set condition} {
    upvar 1 $elementName element
    foreach element $set {
        if {[uplevel 1 $condition]} {return 1}
    }
    return 0

 }
 #--------------- self-test
 if {[file tail [info script]]==[file tail $argv0]} {
    proc P {x y z} {
        expr {$x<3 && $y==5 && $z>6}
    }
    set A {1 2 3}
    set B {4 5 6}
    set C {7 8 9}
    set res [forall a $A {
        exists b $B {
            forall c $C {P $a $b $c}
        }
    }]
    puts res:$res 
 }

adapted from the chat:

dkf
forall and exists are the classic operators of first-order logic (FOL) though they are obviously easy to lift to higher order logic (if you want to get more fun, try selecting the sets for the inner operations - or even snippets of Tcl code - using the outer operations)
dkf
The most useful way of doing things with forall/exists is to have a variable, a set, a selector (to restrict the set) and some general condition which we're testing forall/exists.
 forall A {{a b c} {b c d} {c d e}} {exists x $A {string equal $x "c"}} 
 forall A {equal match} {exists B {aaa a*} {string $A $B aaa}} 
 forall A {{string equal} {string match} regexp} {eval $A a a} 

RS has a feeling that this is structurally very similar to KBK's code in Solving Cryptarithms, on one hand, and to Streams on the other: nested uplevels, explicitly evalled, build up (mildly) complex structures of reasoning, logic, or data flow...


Playing predicate logic | Playing first-order logic | Arts and crafts of Tcl-Tk programming