Définir la notion de « paires » en utilisant la logique d'ordre supérieur

Question

Révise pour un cours sur le raisonnement automatisé et je ne comprends pas comment répondre à cette question:

Montrer comment la notion de paires (x, y) peut être défini logique d'ordre supérieur utilisant une abstraction lambda. Définir une fonction π1 qui retourne le premier élément d'une telle paire. Enfin, montrez que π1(x, y) = x.

J'ai trouvé des questions similaires sur stackoverflow, mais elles sont toutes liées à un schéma, que je n'ai jamais utilisé. Une explication en anglais/notation mathématique pertinente serait appréciée

Answer 1

paires ou tuples décrit les produits du domaine, est l'union de tous les éléments de l'ensemble A et tous les éléments de l'ensemble B:

A × B = { (a, b) | a ∈ A, b ∈ B } 

Ici, A et B sont des types diférents, donc si par exemple vous êtes dans un programme laguage comme C, Java, vous pouvez avoir deux comme (String, Integer), (Char, Boolean), (Double, Double)

maintenant, la fonction π1, est juste une fonction qui prend une paire et renvoie le premier élément, cette fonction est généralement appelée first, et voilà comment il ressemble π1(x, y) = x, d'autre part, vous avez deuxième, faire la même chose, mais ramener le deuxième élément:

fst(a, b) = a 
snd(a, b) = b 

Lorsque j'ai étudié la signature « Caractéristiques des langages de programmation » dans collège notre professeur a recommandé ce book, voir le chapitre Product Domain pour bien comprendre tous ces concepts.

Answer 2

Le sujet principal de cette question est de comprendre comment les données peuvent être représentées en tant que fonctions. Lorsque vous travaillez avec d'autres paradigmes, la façon normale de penser est "data = quelque chose qui est stocké dans une variable" (peut être un tableau, un objet, quelle que soit la structure que vous voulez). Mais quand nous sommes en programmation fonctionnelle, nous pouvons aussi représenter des données en tant que fonctions. Alors disons que vous voulez une paire de fonction (x, y)

Ceci est « pseudo » langage Lisp:

(function pair x y = 
    lambda(pick) 
     if pick = 1 return x 
     else return y ) 

Cet exemple, montre une fonction qui renvoie une fonction lambda qui attend un paramètre.

(function pi this-is-pair = this-is-pair 1) 

this-is-pair doit être construit avec une fonction paire, par conséquent, le paramètre est une fonction qui attend un autre paramètre (pick).

Et maintenant, vous pouvez tester ce que vous avez besoin

(pi (pair x y)) should return x 

Je recommande vivement de voir cette vidéo sur compound data. La plupart des exemples sont faits sur lisp, mais c'est génial de comprendre un concept comme ça.

Answer 3

Ici, vous allez

PAIR := λx. λy. λp. p x y 

π1 := λp. p (λx. λy. x) 

π2 := λp. p (λx. λy. y) 

π1 (PAIR a b) => a 

π2 (PAIR a b) => b 

Vérifiez l'entrée de wiki sur Church encoding pour quelques bons exemples aussi