Paweł Balawender (Mar 24 2025 at 19:31): Paweł Balawender (Mar 24 2025 at 19:31):Hey, I'm trying to define I combinator (I = CKK) in BCK combinatory calculus, but it seems like Isabelle is unable to see a proper unification of the remaining types from C and K combinators. I tried a solution from another thread using TYPE('b) => ...,, but to no effect. What is the reason of this?
theory example
imports Main
begin
definition C :: "('a => 'b => 'c) => 'b => 'a => 'c" where
"C f g x = f x g"
definition K :: "'a => 'b => 'a" where
"K x y = x"
(* cannot get it to work *)
definition I :: "'a => 'a" where
"I = C K K"
end
I only get a warning:
Additional type variable(s) in specification of "I": 'b, 'c
definition I :: "'a => 'a" where
"I = (C:: _ ⇒ ('a ⇒ 'a ⇒ 'a) ⇒ ('a ⇒ 'a)) K K"
if you want to fix them
Paweł Balawender (Mar 24 2025 at 19:38):Oh.. i thought it was an error xD thank you then! Btw, what I'm actually trying to do is to use Isabelle's unification to obtain any specific type inferred for CKK (so, in the above definition, what does 'b evaluate to etc.). Do you have any pointers how to access this from the level of a tactic?
Paweł Balawender (Mar 24 2025 at 19:40):Mathias Fleury said:
definition I :: "'a => 'a" where "I = (C:: _ ⇒ ('a ⇒ 'a ⇒ 'a) ⇒ ('a ⇒ 'a)) K K"
Oh, that's neat, thanks! Actually, this specific instantiation of C is exactly what I'd like to obtain programatically. So to not have to come up with specific type of C on my own, but to use type system to get this thing
Mathias Fleury (Mar 24 2025 at 19:43):On the ML level it is easy:
ML ‹
case @{term ‹C K›} of
Const(_, _) $ s => s›
that is pretty much how I came up with the type (using term "C K" actually)
Paweł Balawender (Mar 24 2025 at 19:46):That's neat! Thank you a lot :)
Last updated: Apr 18 2025 at 20:21 UTC