Hi Bill,
| John, thanks for the Currying info. BTW I'm including below an
| explanation of Curry's paradoxical Y combinator, which in the
| lambda_calculus defines recursive functions.
Thanks, that's an interesting discussion! HOL really is built on top
of typed lambda calculus, so ultimately all terms are those of lambda
calculus, with logical connectives and other constructs merely being
implemented by constants. You can see the underlying abstract syntax
for terms if you remove the special prettyprinting, e.g.
#remove_printer print_qterm;;
# `!x. SUC x = x + 1`;;
val it : term =
Comb (Const ("!", `:(num->bool)->bool`),
Abs (Var ("x", `:num`),
Comb
(Comb (Const ("=", `:num->num->bool`),
Comb (Const ("SUC", `:num->num`), Var ("x", `:num`))),
Comb (Comb (Const ("+", `:num->num->num`), Var ("x", `:num`)),
Comb (Const ("NUMERAL", `:num->num`),
Comb (Const ("BIT1", `:num->num`), Const ("_0", `:num`)))))))
Even for such a small term, this is not very readable, but it can be
instructive if you want to see how certain derived constructs like
`[a;b;c]`, `{x,y}` and `if p then q else r` actually map down into
the underlying abstract syntax of typed lambda-calculus.
John.
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
