forall

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}}}

The implementation is:

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...

aspect is reminded of two procs I have in my prelude:

## WARNING: I do not endorse these implementations for use with >2 args.
## The signature in that case should probably be [all cmdPrefix ls ?ls ...?]

# all ?cmdPrefix ..? $ls
proc all {args} {
    set ls [lindex $args end]
    set cmd [lrange $args 0 end-1]
    if {$cmd eq ""} {
        set cmd K
    }
    foreach x $ls {
        if {![uplevel 1 {*}$cmd [list $x]]} {return false}
    }
    return true
}

# any ?cmdPrefix ..? $ls
proc any {args} {
    set ls [lindex $args end]
    set cmd [lrange $args 0 end-1]
    if {$cmd eq ""} {
        set cmd K
    }
    foreach x $ls {
        if {[uplevel 1 {*}$cmd [list $x]]} {return true}
    }
    return false
}

These permit an interesting implementation of the above:

proc forall {name set cond} {
   all [uplevel 1 [list lmap $name $set $cond]
}
proc forall {name set cond} {
   any [uplevel 1 [list lmap $name $set $cond]
}

With an implementation of function composition, this approaches (modulo scope) the even simpler: interp alias {} forall {} {*}compose all lmap, but the proof of this proposition is unfortunately too large to fit in this margin (that is to say, my implementation of compose would draw in enough code to triple the length of this page and I'd have to introduce all the helpers - yuck).