Chuyển bộ gõ


Từ điển Máy Tính - Foldoc Dictionary
name capture



name capture

(reduction)   In beta reduction, when a term containing a free occurrence of a variable v is substituted into another term where v is bound the free v becomes spuriously bound or "captured". E.g.

 (\ x . \ y . x y) y  -->  \ y . y y (WRONG) 
This problem arises because two distinct variables have the same name. The most common solution is to rename the bound variable using alpha conversion:

 (\ x . \ y' . x y') y --> \ y' . y y' 
Another solution is to use de Bruijn notation.

Note that the argument expression, y, contained a free variable. The whole expression above must therefore be notionally contained within the body of some lambda abstraction which binds y. If we never reduce inside the body of a lambda abstraction (as in reduction to weak head normal form) then name capture cannot occur.

Last updated: 1995-03-14




Giới thiệu VNDIC.net | Plugin từ diển cho Firefox | Từ điển cho Toolbar IE | Tra cứu nhanh cho IE | Vndic bookmarklet | Học từ vựng | Vndic trên web của bạn

© Copyright 2006-2024 VNDIC.NET & VDICT.CO all rights reserved.