Hola, no entiendo el ejercicio 5. No se que son I, K y S y no entiendo la notación de las formulas.
Me podrían explicar?
Saludos
Hola.
El cálculo SKI es un sistema lógico combinatorio y un sistema computacional. Es importante en la teoría matemática de los algoritmos porque es un lenguaje Turing completo, extremadamente simple. Se puede comparar con una versión reducida del cálculo lambda sin tipo. Fue presentado por Moses Schönfinkel y Haskell Curry.
Mas allá de lo anterior, este ejercicio pide simplemente formalizar estos tres operadores y probar una propiedad sobre ellos. Por ejemplo, la definción genércia del operador K sería:
Definition opK (A: Set) (B: Set) (c: A) (x: B) := c.
o equivalentemente, por ejemplo:
Definition opK (A: Set) (B: Set) := fun (c: A) (x: B) => c.
Saludos, Carlos
Ok, gracias Carlos.
Me quedo asi:
(* 5.1 *)
Definition opI (A:Set) (x:A) := x.
Definition opK (A: Set) (B: Set) (x: A) (y: B) := x.
Definition opS (A: Set) (B: Set) (C: Set) (f: A -> B ->C) (g: A -> B) (x:A) := f x (g x).
Check opI.
Check opK.
Check opS.
La parte 5.2 no entiendo como se plantea el Lema. Me podrás ayudar en eso?
Saludos
Me quedo asi:
(* 5.1 *)
Definition opI (A:Set) (x:A) := x.
Definition opK (A: Set) (B: Set) (x: A) (y: B) := x.
Definition opS (A: Set) (B: Set) (C: Set) (f: A -> B ->C) (g: A -> B) (x:A) := f x (g x).
Check opI.
Check opK.
Check opS.
La parte 5.2 no entiendo como se plantea el Lema. Me podrás ayudar en eso?
Saludos
Hola.
Para formalizar el lemma SKK=I va a ser necesario poner los tipos adecuados. Esto es, determinar los tipos ?i en:
Lemma e52 : forall ... : Set, (opS ?1 ?2 ?3 (opK ?4 ?5) (opK ?6 ?7)) = opI ?8.
Una ayuda con los dos primeros: ?1 puede ser un tipo A y ?2: una flecha (función) como: B -> A.
Saludos, Carlos